mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p✝ p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective ⇑f
p : Submodule R M
⊢ ∀ (x y : ↥p),
    (Equiv.Set.image (⇑f) (↑p) i).toFun (x + y) =
      (Equiv.Set.image (⇑f) (↑p) i).toFun x + (Equiv.Set.image (⇑f) (↑p) i).toFun y

Tactic:
intros
      simp only [coe_add, map_add, Equiv.toFun_as_coe, Equiv.Set.image_apply]
      rfl

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝ : M₀
⊢ Commute 0 x✝

Tactic:
commute_iff_eq,

Goal state after:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝ : M₀
⊢ 0 * x✝ = x✝ * 0
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocSemiring M
n : ℕ
x✝ : M
⊢ Commute (↑n) x✝

Tactic:
commute_iff_eq,

Goal state after:
M : Type u_1
inst✝ : NonAssocSemiring M
n : ℕ
x✝ : M
⊢ ↑n * x✝ = x✝ * ↑n
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n : ℤ
x✝ : M
⊢ Commute (↑n) x✝

Tactic:
commute_iff_eq,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n : ℤ
x✝ : M
⊢ ↑n * x✝ = x✝ * ↑n
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝ : M
⊢ Commute (a + b) x✝

Tactic:
commute_iff_eq,

Goal state after:
M : Type u_1
inst✝ : Distrib M
a b : M
ha : a ∈ center M
hb : b ∈ center M
x✝ : M
⊢ (a + b) * x✝ = x✝ * (a + b)
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝ : M
⊢ Commute (-a) x✝

Tactic:
commute_iff_eq,

Goal state after:
M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝ : M
⊢ -a * x✝ = x✝ * -a
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: case inl
R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
left✝ : 0 = 0
h : 1 = 0
⊢ False

pp: case inr
R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
h : 1 = 0
right✝ : 0 = 0
⊢ False

Tactic:
· exact zero_ne_one h.symm

Goal state after:
case inr
R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
h : 1 = 0
right✝ : 0 = 0
⊢ False
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: case inr
R : Type u_6
S : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
h : 1 = 0
right✝ : 0 = 0
⊢ False

Tactic:
· exact zero_ne_one h.symm

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x : R
hx : x ∈ ↑(Submonoid.closure s)
this : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x
t : List R
ht1 : ∀ y ∈ t, y ∈ s
ht2 : t.prod = x
⊢ t.prod = x

Tactic:
ht2

Goal state after:
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x : R
hx : x ∈ ↑(Submonoid.closure s)
this : ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x
t : List R
ht1 : ∀ y ∈ t, y ∈ s
ht2 : t.prod = x
⊢ x = x
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
this : a ^ n.succ * x ^ n = p * y
hdvdx : p ∣ x ^ n
⊢ p ^ 2 ∣ p * x

Tactic:
obtain ⟨z, rfl⟩ := hp.dvd_of_dvd_pow hdvdx

Goal state after:
case inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
y z : M
hb : ¬p ^ 2 ∣ p * (p * z)
hbdiv : p ∣ (p * (p * z)) ^ n
hy : a ^ n.succ * (p * (p * z)) ^ n = p ^ n.succ * y
this : a ^ n.succ * (p * z) ^ n = p * y
hdvdx : p ∣ (p * z) ^ n
⊢ p ^ 2 ∣ p * (p * z)
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case left
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * a = 0
⊢ x * (a * b) = 0

Tactic:
rw [← mul_assoc, h', zero_mul]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case mpr
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
x✝ : ∃ x, x * a = 0 ∧ x ≠ 0
b : M₀
hb₁ : b * a = 0
hb₂ : b ≠ 0
⊢ Associates.mk b * Associates.mk a = 0

Tactic:
Associates.mk_mul_mk,

Goal state after:
case mpr
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
x✝ : ∃ x, x * a = 0 ∧ x ≠ 0
b : M₀
hb₁ : b * a = 0
hb₂ : b ≠ 0
⊢ Associates.mk (b * a) = 0
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Zero β
inst✝ : SMulZeroClass α β
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ s • 0

Tactic:
by simpa [mem_smul] using! hs

Goal state after:
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₂ ≃ₐ[R] A₂'
a✝ : A₂
⊢ ((fun ψ ↦ e.symm.trans (ψ.trans e')) ((fun ψ ↦ e.trans (ψ.trans e'.symm)) ψ)) a✝ = ψ a✝

Tactic:
simp_rw [trans_apply, apply_symm_apply]

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
h : a ≤ b
⊢ ∃ a', Disjoint a a' ∧ a ⊔ a' = b

Tactic:
simp_rw [disjoint_iff]
  apply exists_inf_eq_and_sup_eq (by simp) h

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ (⨅ c, ⨆ x, b ⊓ bif x then c else cᶜ) ≤ sSup {a | IsAtom a ∧ a ≤ ⨅ c, ⨆ x, b ⊓ bif x then c else cᶜ}

Tactic:
iInf_iSup_eq,

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ (⨆ g, ⨅ a, b ⊓ bif g a then a else aᶜ) ≤ sSup {a | IsAtom a ∧ a ≤ ⨆ g, ⨅ a, b ⊓ bif g a then a else aᶜ}
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type ?u.8
inst✝ : CompleteAtomicBooleanAlgebra α
A : α
⊢ (fun S ↦ sSup (Subtype.val '' S)) ((fun A ↦ {a | ↑a ≤ A}) A) = A

Tactic:
by simp [Subtype.coe_image]

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_3.refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx : x✝ ∈ span R S
x y : M
X : Finset M
hX : ↑X ⊆ S
hxX : x ∈ span R ↑X
Y : Finset M
hY : ↑Y ⊆ S
hyY : y ∈ span R ↑Y
⊢ ∃ y_1 ∈ span R ↑X, ∃ z ∈ span R ↑Y, y_1 + z = x + y

Tactic:
exact ⟨x, hxX, y, hyY, rfl⟩

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case sup
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊔ b ∈ f '' latticeClosure s

pp: case right.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊓ b ∈ f '' latticeClosure s

Tactic:
· rintro _ - _ - ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩
    exact ⟨a ⊔ b, isSublattice_latticeClosure.supClosed ha hb, map_sup ..⟩

Goal state after:
case right.inf
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊓ b ∈ f '' latticeClosure s
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_8
A : Type u_9
inst✝⁴ : Semiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x : A
h : ∀ y ∈ s, Commute y x
y : A
hy : y ∈ span R s
⊢ Commute y x

Tactic:
induction hy using span_induction with
  | mem _ _ => aesop
  | zero => exact .zero_left _
  | add _ _ _ _ h₁ h₂ => exact h₁.add_left h₂
  | smul _ _ _ h => exact h.smul_left _

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ (∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x) →
    ∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

pp: case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ (∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id) →
    ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x

Tactic:
· intro hk s hsup
      -- Consider the set of finite joins of elements of the (plain) set s.
      let S : Set α := { x | ∃ t : Finset α, ↑t ⊆ s ∧ x = t.sup id }
      -- S is directed, nonempty, and still has sup above k.
      have dir_US : DirectedOn (· ≤ ·) S := by
        rintro x ⟨c, hc⟩ y ⟨d, hd⟩
        use x ⊔ y
        constructor
        · use c ∪ d
          constructor
          · simp only [hc.left, hd.left, Set.union_subset_iff, Finset.coe_union, and_self_iff]
          · simp only [hc.right, hd.right, Finset.sup_union]
        simp only [and_self_iff, le_sup_left, le_sup_right]
      have sup_S : sSup s ≤ sSup S := by
        apply sSup_le_sSup
        intro x hx
        use {x}
        simpa only [and_true, id, Finset.coe_singleton, eq_self_iff_true,
          Finset.sup_singleton, Set.singleton_subset_iff]
      have Sne : S.Nonempty := by
        suffices ⊥ ∈ S from Set.nonempty_of_mem this
        use ∅
        simp
      -- Now apply the defn of compact and finish.
      obtain ⟨j, ⟨hjS, hjk⟩⟩ := hk S Sne dir_US (le_trans hsup sup_S)
      obtain ⟨t, ⟨htS, htsup⟩⟩ := hjS
      use t
      exact ⟨htS, by rwa [← htsup]⟩

Goal state after:
case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
⊢ (∀ (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id) →
    ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_2
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 1) (f 0 ⊔ f 2)

pp: case refine_3
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 2) (f 0 ⊔ f 1)

pp: case refine_4
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
x✝ : Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
i : Fin 3
h₀ : Disjoint (f 0) (f 1 ⊔ f 2)
h₁ : Disjoint (f 1) (f 0 ⊔ f 2)
h₂ : Disjoint (f 2) (f 0 ⊔ f 1)
⊢ Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)

Tactic:
· simpa using h 1

Goal state after:
case refine_3
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
h : ∀ (i : Fin 3), Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
⊢ Disjoint (f 2) (f 0 ⊔ f 1)

case refine_4
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
x✝ : Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 0 ⊔ f 2) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
i : Fin 3
h₀ : Disjoint (f 0) (f 1 ⊔ f 2)
h₁ : Disjoint (f 1) (f 0 ⊔ f 2)
h₂ : Disjoint (f 2) (f 0 ⊔ f 1)
⊢ Disjoint (f i) (⨆ j, ⨆ (_ : j ≠ i), f j)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
t : Set ι
hf : iSupIndep f
s : Finset ι
⊢ Disjoint (↑s) t → Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)

Tactic:
hst

Goal state after:
α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
t : Set ι
hf : iSupIndep f
s : Finset ι
hst : Disjoint (↑s) t
⊢ Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ∅.sup id
⊢ sSup s ∈ s

pp: case inr
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ sSup s ∈ s

Tactic:
· rw [Finset.sup_empty] at ht₂
    rw [ht₂]
    simp [eq_singleton_bot_of_sSup_eq_bot_of_nonempty ht₂ hne]

Goal state after:
case inr
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ sSup s ∈ s
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y : N
hx : x ∈ span R s
hy : y ∈ span R t
⊢ (B x) y ∈ P'

Tactic:
induction hx, hy using span_induction₂ with

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_4
inst✝² : CommSemiring R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
s : Finset κ
g : ι → κ → R
⊢ ∑ f ∈ piFinset fun x ↦ s, ∏ i, g i (f i) = ∏ i, ∑ j ∈ s, g i j

Tactic:
rw [← prod_univ_sum]

Goal state after:
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H : Type u_8
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
v : α →₀ M
b : β
this : DecidableEq β
⊢ {x | x ∈ v.support.val ∧ f x = b}.Subsingleton

Tactic:
intro x; grind

Goal state after:
Module: Mathlib.Data.Finsupp.Indicator

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
a : ι
f : (j : ι) → j ∈ {a} → α
⊢ indicator {a} f = single a (f a ⋯)

Tactic:
by
  classical
  ext j
  simp only [single_apply, indicator_apply, mem_singleton, @eq_comm _ a j]
  split_ifs with h <;> simp [h]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋃ i, s i
⊢ f x = ⨆ i, (s i).mulIndicator f x

Tactic:
rw [mem_iUnion] at hx

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : ∃ i, x ∈ s i
⊢ f x = ⨆ i, (s i).mulIndicator f x
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ ∀ (a : α) (s : Multiset α),
    ((∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod) →
      (∀ (a_2 : α), a_2 ∈ a ::ₘ s → p a_2) → f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Tactic:
intro a s hs hpsa

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
a : α
b : β
m : M
⊢ (single a (single b m)).uncurry = single (a, b) m

Tactic:
by
  ext ⟨x, y⟩
  rcases eq_or_ne a x with rfl | hne <;> classical simp [single_apply, *]

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: m n : ℕ
⊢ range (natAdd m) = {i | m ≤ ↑i}

Tactic:
by
  ext i
  constructor
  · rintro ⟨i, rfl⟩
    apply le_coe_natAdd
  · refine fun (hi : m ≤ i) ↦ ⟨⟨i - m, by lia⟩, ?_⟩
    ext
    simp [hi]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
⊢ (ι →₀ R) ≃ₗ[R] ι →₀ R

Tactic:
refine .ofLinearMap (linearCombination _ fun j ↦ single j 1 + single i (c j))
    (linearCombination _ fun j ↦ single j 1 - single i (c j)) ?_ ?_ <;>
  ext j k <;> obtain rfl | hk := eq_or_ne i k
  · simp [h₀]
  · simp [hk]
  · simp [h₀]
  · simp [hk]

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
x : α
u : Fin 0 → α
⊢ Set.range (vecCons x u) = {x}

Tactic:
by
  rw [range_cons, range_empty, Set.union_empty]

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : Fin n
h : i ≤ m.castSucc
⊢ (finSuccEquiv' i) m.succ = some m

Tactic:
by
  rw [← Fin.succAbove_of_le_castSucc _ _ h, finSuccEquiv'_succAbove]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
t : ι → Set α
h : Pairwise (Disjoint on t)
ht : ∀ (i : ι), (t i).Finite
val✝ : Fintype ι
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ i, t i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a

Tactic:
lift t to ι → Finset α using ht

Goal state after:
case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i ↦ ↑(t i))
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ i, (fun i ↦ ↑(t i)) i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i ↦ ↑(t i)) i), f a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset hf, f i

Tactic:
rw [finprod_cond_eq_prod_of_cond_iff f (fun hx => h _ hx), Finset.sdiff_singleton_eq_erase]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
⊢ f a * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab = ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)

Tactic:
finprod_mem_finset_product'

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b) =
    ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (abc : α × β × γ) (_ : abc ∈ s), f abc = ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)

Tactic:
finprod_mem_finset_product'

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (a : α) (b : β × γ) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b) =
    ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (a : α) (b : β × γ) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b) =
    ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)

Tactic:
finprod_mem_finset_product'

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (a : α) (a_1 : β) (b : γ) (_ :
      b ∈ Finset.image Prod.snd ({ab ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}) | ab.1 = a_1})), f (a, a_1, b) =
    ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x y : ι →₀ R
hxy : (linearCombination R ⇑b) x = (linearCombination R ⇑b) y
⊢ x = y

Tactic:
← b.repr_linearCombination x,

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x y : ι →₀ R
hxy : (linearCombination R ⇑b) x = (linearCombination R ⇑b) y
⊢ b.repr ((linearCombination R ⇑b) x) = y
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.top
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ (⊤ + z) = x ^ ⊤ * x ^ z

Tactic:
top_add,

Goal state after:
case inr.inr.top
x y z : ℕ∞
x_2 : 1 < x
⊢ x ^ ⊤ = x ^ ⊤ * x ^ z
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inr.inr.inr
x y z : ℕ∞
x_2 : 1 < x
y_2 : 1 < y
⊢ (x * y) ^ ⊤ = ⊤ * y ^ ⊤

Tactic:
epow_top y_2,

Goal state after:
case top.inr.inr.inr.inr
x y z : ℕ∞
x_2 : 1 < x
y_2 : 1 < y
⊢ (x * y) ^ ⊤ = ⊤ * ⊤
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
⊢ LinearIndepOn R v ↑s ↔ ∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i

Tactic:
classical
  simp_rw [LinearIndepOn, Fintype.linearIndependent_iffₛ]
  constructor
  · rintro hv f g hfg i hi
    simp_rw [← s.sum_attach] at hfg
    exact hv (f ∘ Subtype.val) (g ∘ Subtype.val) hfg ⟨i, hi⟩
  · rintro hv f g hfg i
    simpa using hv (fun j ↦ if hj : j ∈ s then f ⟨j, hj⟩ else 0)
      (fun j ↦ if hj : j ∈ s then g ⟨j, hj⟩ else 0) (by simpa +contextual [← s.sum_attach]) i

Goal state after:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a b : Fin n
⊢ ∏ i ∈ Ioo (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Ioo a b, f (Fin.cast h i)

Tactic:
simp [← map_finCongr_Ioo]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ (∏ i, ∏ j ≥ i, f i.castSucc j) * ∏ i, ∏ j ≥ i, f j.succ i = ∏ i, ∏ j ≥ i, f i.castSucc j * f j.succ i

Tactic:
by
    simp only [Finset.prod_mul_distrib]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ n.Coprime (n - m) ↔ n.Coprime m

Tactic:
by
  rw [Coprime, Coprime, gcd_self_sub_right h]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
⊢ hv.repr.ker = ⊥

Tactic:
by
  rw [LinearIndependent.repr, LinearEquiv.ker]

Goal state after: