mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝⁴ : FunLike F α β
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
f : sSupHom β γ
g : sSupHom α β
s : Set α
⊢ sSup (⇑f '' ⇑g '' s) = sSup (⇑f ∘ ⇑g '' s)

Tactic:
Set.image_image

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝⁴ : FunLike F α β
inst✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
f : sSupHom β γ
g : sSupHom α β
s : Set α
⊢ sSup ((fun x ↦ f (g x)) '' s) = sSup (⇑f ∘ ⇑g '' s)
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
⊢ a⁻¹ ∈ s.centralizer

Tactic:
rintro c hc
    rw [mul_inv_eq_iff_eq_mul₀ ha₀, mul_assoc, eq_inv_mul_iff_mul_eq₀ ha₀, ha c hc]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ f (a * (algebraMap R A) r) = f a * (algebraMap R B) r

Tactic:
← Algebra.commutes,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ f ((algebraMap R A) r * a) = f a * (algebraMap R B) r
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ f ((algebraMap R A) r * a) = f a * (algebraMap R B) r

Tactic:
← Algebra.commutes,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ f ((algebraMap R A) r * a) = (algebraMap R B) r * f a
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
hf : f 1 = 1
r : R
h : Invertible ((algebraMap R A) r)
⊢ f ⅟((algebraMap R A) r) * (algebraMap R B) r = 1

Tactic:
← Algebra.commutes,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
hf : f 1 = 1
r : R
h : Invertible ((algebraMap R A) r)
⊢ (algebraMap R B) r * f ⅟((algebraMap R A) r) = 1
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case mp.add
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x y : R
hx✝ : x ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
hy✝ : y ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
hL : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
hM : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = y
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x + y

Tactic:
obtain ⟨⟨L, HL1, HL2⟩, ⟨M, HM1, HM2⟩⟩ := And.intro hL hM

Goal state after:
case mp.add
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x y : R
hx✝ : x ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
hy✝ : y ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
hL : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
hM : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = y
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s
HL2 : (List.map List.prod L).sum = x
M : List (List R)
HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s
HM2 : (List.map List.prod M).sum = y
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x + y
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case add
R : Type u_1
inst✝ : Ring R
s : Set R
x x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hL : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x✝
hM : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = y✝
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x✝ + y✝

Tactic:
obtain ⟨⟨L, HL1, HL2⟩, ⟨M, HM1, HM2⟩⟩ := And.intro hL hM

Goal state after:
case add
R : Type u_1
inst✝ : Ring R
s : Set R
x x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hL : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x✝
hM : ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = y✝
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1
HL2 : (List.map List.prod L).sum = x✝
M : List (List R)
HM1 : ∀ t ∈ M, ∀ y ∈ t, y ∈ s ∨ y = -1
HM2 : (List.map List.prod M).sum = y✝
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod L).sum = x✝ + y✝
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
hhd : hd ∈ s
⊢ (hd :: tl).prod = -(hd :: L).prod

Tactic:
by rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x y : M
⊢ x ~ᵤ y ↔ x = y

Tactic:
simp [Associated, Units.eq_one]

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

Goal state before:
pp: case zero
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ Associates.mk (a ^ 0) = Associates.mk a ^ 0

Tactic:
simp [*, pow_succ, Associates.mk_mul_mk.symm]

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

Goal state before:
pp: case succ
M : Type u_1
inst✝ : CommMonoid M
a : M
n✝ : ℕ
a✝ : Associates.mk (a ^ n✝) = Associates.mk a ^ n✝
⊢ Associates.mk (a ^ (n✝ + 1)) = Associates.mk a ^ (n✝ + 1)

Tactic:
simp [*, pow_succ, Associates.mk_mul_mk.symm]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ (¬IsUnit a ∧ ∀ (a_1 a_2 : M), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) ↔
    ¬IsUnit a ∧ ∀ ⦃a_1 b : M⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b

Tactic:
apply Iff.rfl.and

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ (∀ (a_1 a_2 : M), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) ↔ ∀ ⦃a_1 b : M⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b
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 : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁ →ₐ[R] A₂
⊢ (fun f ↦ ((↑e₂.symm).comp f).comp ↑e₁) ((fun f ↦ ((↑e₂).comp f).comp ↑e₁.symm) f) = f

Tactic:
simp only [AlgHom.comp_assoc, symm_comp]
    simp only [← AlgHom.comp_assoc, symm_comp, AlgHom.id_comp, AlgHom.comp_id]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case inl
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
N : Submodule R M
s t : Set S
r✝ : S
n✝ : M
hr : r✝ ∈ s
hn : n✝ ∈ N
⊢ r✝ • n✝ ∈ s • N ⊔ t • N

Tactic:
exact Submodule.mem_sup_left (mem_set_smul_of_mem_mem hr hn)

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: α : Type u_2
ι : Type u_5
κ : Type u_6
inst✝ : DistribLattice α
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → α
⊢ s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' ⋯ fun i ↦ f i.1 ⊓ g i.2

Tactic:
by
  simp_rw [Finset.sup'_inf_distrib_right, Finset.sup'_inf_distrib_left, sup'_product_left]

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ c (y ⊔ x) = c (x ⊔ y)

Tactic:
sup_comm (a := x)

Goal state after:
α : Type u_1
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ c (y ⊔ x) = c (y ⊔ x)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case smul.mem
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
r₁ : R
y x✝ : M
h : x✝ ∈ univ • s
⊢ r₁ • x✝ ∈ closure (univ • s)

Tactic:
obtain ⟨r₂, -, x, hx, rfl⟩ := h
        exact subset_closure ⟨r₁ * r₂, trivial, x, hx, mul_smul ..⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K < H ∧ H < L ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K

Tactic:
rw [lt_iff_le_and_ne, lt_iff_le_not_ge, and_and_and_comm]

Goal state after:
A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ span R 0 = ⊥

Tactic:
← singleton_zero,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ R ∙ 0 = ⊥
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
b : α
hbS : b ∈ S
x✝ : ⊥ ∈ {a | a ≤ sSup S ∧ IsAtom a}
hale : ⊥ ≤ sSup S
hatom : IsAtom ⊥
hba : ⊥ ≤ b
⊢ ⊥ ∈ S

pp: case inr
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
a : α
x✝ : a ∈ {a | a ≤ sSup S ∧ IsAtom a}
hale : a ≤ sSup S
hatom : IsAtom a
hbS : a ∈ S
hba : a ≤ a
⊢ a ∈ S

Tactic:
· simpa using hatom.1

Goal state after:
case inr
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
a : α
x✝ : a ∈ {a | a ≤ sSup S ∧ IsAtom a}
hale : a ≤ sSup S
hatom : IsAtom a
hbS : a ∈ S
hba : a ≤ a
⊢ a ∈ S
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
t : Finset M
ht : ↑t ⊆ ↑(span R s)
⊢ ∃ T, ↑T ⊆ s ∧ ↑t ⊆ ↑(span R ↑T)

Tactic:
classical
  induction t using Finset.induction_on with
  | empty => exact ⟨∅, by simp⟩
  | insert a t hat IH =>
    obtain ⟨T, hTs, htT⟩ := IH (by simp_all [Set.insert_subset_iff])
    obtain ⟨T', hT's, haT'⟩ := mem_span_finite_of_mem_span (ht (Finset.mem_insert_self _ _))
    refine ⟨T ∪ T', by simp_all, ?_⟩
    simp only [Finset.coe_insert, Finset.coe_union, span_union, insert_subset_iff, SetLike.mem_coe]
    exact ⟨mem_sup_right haT', htT.trans (le_sup_left (a := span R _))⟩

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
t : Finset ι
x✝² : t ⊆ s
i : ι
x✝¹ : i ∈ s
x✝ : i ∉ t
⊢ Disjoint ((fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩) i) (t.sup fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩)

pp: case refine_2
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
i : ι
x✝³ : i ∈ s
t : Finset (β i)
x✝² : t ⊆ g i
j : β i
x✝¹ : j ∈ g i
x✝ : j ∉ t
⊢ Disjoint ((fun b ↦ f ⟨i, b⟩) j) (t.sup fun b ↦ f ⟨i, b⟩)

Tactic:
· let u := (g i).map (Function.Embedding.sigmaMk i)
    let v := t.biUnion (fun j => (g j).map (Function.Embedding.sigmaMk j))
    suffices Disjoint (u.sup f) (v.sup f) by simpa only [sup_map, sup_biUnion, u, v]
    apply SupIndep.disjoint_sup_sup h <;> grind [disjoint_left]

Goal state after:
case refine_2
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
h : (s.sigma g).SupIndep f
i : ι
x✝³ : i ∈ s
t : Finset (β i)
x✝² : t ⊆ g i
j : β i
x✝¹ : j ∈ g i
x✝ : j ∉ t
⊢ Disjoint ((fun b ↦ f ⟨i, b⟩) j) (t.sup fun b ↦ f ⟨i, b⟩)
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F : Type u_3
α : Type u_5
β : Type u_6
inst✝³ : FunLike F α β
inst✝² : One F
inst✝¹ : One β
inst✝ : IsOneApply F α β
f : F
⊢ ⇑f = 1 ↔ f = 1

Tactic:
by
  constructor
  · intro h
    simp [DFunLike.ext_iff, h]
  · intro h
    simp [h]

Goal state after:
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: F' : Type u_4
α : Type u_5
inst✝² : FunLike F' α α
inst✝¹ : One F'
inst✝ : IsOneApplyEqSelf F' α
f : F'
⊢ ⇑f = id ↔ f = 1

Tactic:
by
  constructor
  · intro h
    simp [DFunLike.ext_iff, h]
  · intro h
    simp [h]

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
V : Submodule R M
f g : ↥V →ₗ[R] N
S : Set M
hV : V = span R S
⊢ f = g → ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩

Tactic:
rintro rfl _
    rfl

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

Goal state before:
pp: case a
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
hr : IsUnit r
⊢ span R s ≤ span R (r • s)

Tactic:
· convert! span_smul_le (r • s) ((hr.unit⁻¹ :) : R)
    simp [smul_smul]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Finset ι
f : ι → M
g : ι → N
this : DecidableEq ι
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (∏ x ∈ s, f x, ∏ x ∈ s, g x) = ∏ x ∈ s, (f x, g x) →
        (∏ x ∈ insert a s, f x, ∏ x ∈ insert a s, g x) = ∏ x ∈ insert a s, (f x, g x)

Tactic:
by simp +contextual [Prod.ext_iff]

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

Goal state before:
pp: case pos
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : ¬1 < s.card
hcard0 : s.card = 0
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)

Tactic:
grind [Finset.card_eq_zero, Finset.card_eq_one]

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

Goal state before:
pp: case neg
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : ¬1 < s.card
hcard0 : ¬s.card = 0
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)

Tactic:
grind [Finset.card_eq_zero, Finset.card_eq_one]

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

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : {c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
⊢ sSup {c | IsCompactElement c ∧ c ≤ b} = ⊥

Tactic:
sSup_eq_bot

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : {c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
⊢ ∀ a ∈ {c | IsCompactElement c ∧ c ≤ b}, a = ⊥
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case smul_left
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
t : R
u : M
v : N
hu : u ∈ span R s
hv : v ∈ span R t✝
huv : (B u) v ∈ P'
⊢ (B (t • u)) v ∈ P'

Tactic:
| smul_left t u v hu hv huv =>

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
this : x ∈ map (⨆ i ∈ s, p i).subtype (⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i))
⊢ ⟨x, hx⟩ ∈ ⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i)

Tactic:
obtain ⟨y, hy, rfl⟩ := Submodule.mem_map.mp this

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ y : ↥(⨆ i ∈ s, p i)
hy : y ∈ ⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i)
hx : (⨆ i ∈ s, p i).subtype y ∈ ⨆ i ∈ s, p i
x✝ : ⟨(⨆ i ∈ s, p i).subtype y, hx⟩ ∈ ⊤
this : (⨆ i ∈ s, p i).subtype y ∈ map (⨆ i ∈ s, p i).subtype (⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i))
⊢ ⟨(⨆ i ∈ s, p i).subtype y, hx⟩ ∈ ⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i)
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
ha' : a ∉ s
⊢ f a * ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j =
    ∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j

Tactic:
rw [mul_sum]

Goal state after:
case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
ha' : a ∉ s
⊢ ∑ i ∈ s, f a * ((g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) =
    ∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
s : Set M
f g : M →ₛₗ[σ₁₂] M₂
⊢ Set.EqOn ⇑f ⇑g ↑(span R s) ↔ Set.EqOn (⇑f) (⇑g) s

Tactic:
by
  rw [← le_eqLocus, span_le]; rfl

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrder ι
s : Finset ι
f : ι → R
⊢ ∏ i ∈ s, (1 - f i) = 1 - ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 - f j)

Tactic:
rw [prod_sub_ordered]
  simp

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

Goal state before:
pp: case inr
ι : Type u_5
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
hn : n > 0
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

Tactic:
Nat.div_eq_iff_eq_mul_left hn (dvd_sum hf),

Goal state after:
case inr
ι : Type u_5
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
hn : n > 0
⊢ ∑ i ∈ s, f i = (∑ i ∈ s, f i / n) * n
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ (single a b) a' = if a = a' then b else 0

Tactic:
@eq_comm _ a a',

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Decidable (a = a')
⊢ (single a b) a' = if a' = a then b else 0
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ single a (∑ b ∈ s, f b) = ∑ b ∈ s, single a (f b)

Tactic:
trans
  · apply single_multiset_sum
  · rw [Multiset.map_map]
    rfl

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
x : M
⊢ -(↑u • x) = -(u • x)

Tactic:
Units.smul_def

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
x : M
⊢ -(↑u • x) = -(↑u • x)
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: case h
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 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)
l : List α
hps : ∀ (a : α), a ∈ ⟦l⟧ → p a
⊢ f (prod ⟦l⟧) ≤ (map f ⟦l⟧).prod

Tactic:
simp [l.le_prod_of_submultiplicative_on_pred f p h_one hp_one h_mul hp_mul (by simpa)]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : IsOrderedCancelMonoid α
inst✝ : MulLeftStrictMono α
s : Multiset ι
f g : ι → α
hs : s ≠ ∅
hfg : ∀ (i : ι), i ∈ s → f i < g i
⊢ (map f s).prod < (map g s).prod

Tactic:
obtain ⟨i, hi⟩ := exists_mem_of_ne_zero hs

Goal state after:
ι : Type u_1
α : Type u_2
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : IsOrderedCancelMonoid α
inst✝ : MulLeftStrictMono α
s : Multiset ι
f g : ι → α
hs : s ≠ ∅
hfg : ∀ (i : ι), i ∈ s → f i < g i
i : ι
hi : i ∈ s
⊢ (map f s).prod < (map g s).prod
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i

Tactic:
gcongr with j hj <;> aesop

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
i : Finset β
f : β → Multiset α
⊢ i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)

Tactic:
induction i using Finset.cons_induction_on with

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι R M
i j : ι
⊢ b.equivFun (b i) j = if i = j then 1 else 0

Tactic:
by rw [b.equivFun_apply, b.repr_self_apply]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m '' Icc i j = Icc (natAdd m i) (natAdd m j)

Tactic:
← preimage_natAdd_Icc_natAdd,

Goal state after:
n m : ℕ
i j : Fin n
⊢ natAdd m '' natAdd ?m ⁻¹' Icc (natAdd ?m i) (natAdd ?m j) = Icc (natAdd m i) (natAdd m j)

case m
n m : ℕ
i j : Fin n
⊢ ℕ
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
s : Set α
inst✝ : Fintype ↑s
⊢ s ∩ mulSupport f = ↑s.toFinset ∩ mulSupport f

Tactic:
coe_toFinset s

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
e : M ≃ₗ[R] ι → R
j : M
x✝ : ι
⊢ (ofEquivFun e).equivFun j x✝ = e j x✝

Tactic:
simp_rw [Basis.equivFun_apply, Basis.ofEquivFun_repr_apply]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) '' Icc i j = Icc (i.addNat m) (j.addNat m)

Tactic:
rw [← preimage_addNat_Icc_addNat, image_preimage_eq_of_subset]

Goal state after:
n m : ℕ
i j : Fin n
⊢ Icc (i.addNat m) (j.addNat m) ⊆ range fun x ↦ x.addNat m