mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case mem.add
R : Type u
inst✝ : NonAssocRing R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : x ∈ closure s), p x 1 hx ⋯
neg_left : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p (-x) y ⋯ hy
neg_right : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : R
hz : z ∈ s
x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p x✝ z hx✝ ⋯
h₂ : p y✝ z hy✝ ⋯
⊢ p (x✝ + y✝) z ⋯ ⋯

Tactic:
| add _ _ _ _ h₁ h₂ =>

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

Goal state before:
pp: case add
R : Type u
inst✝ : NonAssocRing R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : x ∈ closure s), p x 1 hx ⋯
neg_left : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p (-x) y ⋯ hy
neg_right : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : x ∈ closure s
x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : p x x✝ hx hx✝
h₂ : p x y✝ hx hy✝
⊢ p x (x✝ + y✝) hx ⋯

Tactic:
| add _ _ _ _ h₁ h₂ =>

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

Goal state before:
pp: case add
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h₁ : x✝ ∈ closure s
h₂ : y✝ ∈ closure s
⊢ x✝ + y✝ ∈ closure s

Tactic:
| add _ _ _ _ h₁ h₂ =>

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
this : p₁ ∣ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂

Tactic:
rw [← hp₁.dvd_prime_iff_associated hp₂]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
this : p₁ ∣ p₂ ^ k₂
⊢ p₁ ∣ p₂
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
t : Subring S
h : t ≤ f.range
⊢ map f (comap f t) = t

Tactic:
by
  simpa only [inf_of_le_left h] using Subring.map_comap_eq f t

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 : 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:
by
    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.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
inst✝² : CommSemiring R
inst✝¹ : Semiring A₁
inst✝ : Algebra R A₁
e : A₁ ≃ₐ[R] A₁
n x✝¹ : ℕ
ih : ⇑(e ^ x✝¹) = (⇑e)^[x✝¹]
x✝ : A₁
⊢ (e ^ x✝¹.succ) x✝ = (⇑e)^[x✝¹.succ] x✝

Tactic:
simp [pow_succ, ih]

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
c : ClosureOperator α
x y : α
hy : c.IsClosed y
⊢ c x ≤ y ↔ x ≤ y

Tactic:
by
  rw [← hy.closure_eq, ← le_closure_iff]

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

Goal state before:
pp: case mem.add
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
s : Set M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
t : Set N
p : (x : M) → (y : N) → x ∈ span R s → y ∈ span R t → Prop
mem_mem : ∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯
zero_left : ∀ (y : N) (hy : y ∈ span R t), p 0 y ⋯ hy
zero_right : ∀ (x : M) (hx : x ∈ span R s), p x 0 hx ⋯
add_left :
  ∀ (x y : M) (z : N) (hx : x ∈ span R s) (hy : y ∈ span R s) (hz : z ∈ span R t),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x : M) (y z : N) (hx : x ∈ span R s) (hy : y ∈ span R t) (hz : z ∈ span R t),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
smul_left : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p (r • x) y ⋯ hy
smul_right : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p x (r • y) hx ⋯
a : M
b z : N
hz : z ∈ t
x✝ y✝ : M
hx✝ : x✝ ∈ span R s
hy✝ : y✝ ∈ span R s
h₁ : p x✝ z hx✝ ⋯
h₂ : p y✝ z hy✝ ⋯
⊢ p (x✝ + y✝) z ⋯ ⋯

Tactic:
| add _ _ _ _ h₁ h₂ =>

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

Goal state before:
pp: case add
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
s : Set M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
t : Set N
p : (x : M) → (y : N) → x ∈ span R s → y ∈ span R t → Prop
mem_mem : ∀ (x : M) (y : N) (hx : x ∈ s) (hy : y ∈ t), p x y ⋯ ⋯
zero_left : ∀ (y : N) (hy : y ∈ span R t), p 0 y ⋯ hy
zero_right : ∀ (x : M) (hx : x ∈ span R s), p x 0 hx ⋯
add_left :
  ∀ (x y : M) (z : N) (hx : x ∈ span R s) (hy : y ∈ span R s) (hz : z ∈ span R t),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x : M) (y z : N) (hx : x ∈ span R s) (hy : y ∈ span R t) (hz : z ∈ span R t),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
smul_left : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p (r • x) y ⋯ hy
smul_right : ∀ (r : R) (x : M) (y : N) (hx : x ∈ span R s) (hy : y ∈ span R t), p x y hx hy → p x (r • y) hx ⋯
a : M
b : N
ha : a ∈ span R s
x✝ y✝ : N
hx✝ : x✝ ∈ span R t
hy✝ : y✝ ∈ span R t
h₁ : p a x✝ ha hx✝
h₂ : p a y✝ ha hy✝
⊢ p a (x✝ + y✝) ha ⋯

Tactic:
| add _ _ _ _ h₁ h₂ =>

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

Goal state before:
pp: case add
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x x✝ y✝ : M
hx✝ : x✝ ∈ span R s
hy✝ : y✝ ∈ span R s
h₁ : x✝ ∈ closure (univ • s)
h₂ : y✝ ∈ closure (univ • s)
⊢ x✝ + y✝ ∈ closure (univ • s)

Tactic:
| add _ _ _ _ h₁ h₂ =>

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

Goal state before:
pp: case smul.add
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✝ y✝ : M
hx✝ : x✝ ∈ closure (univ • s)
hy✝ : y✝ ∈ closure (univ • s)
h₁ : r₁ • x✝ ∈ closure (univ • s)
h₂ : r₁ • y✝ ∈ closure (univ • s)
⊢ r₁ • (x✝ + y✝) ∈ closure (univ • s)

Tactic:
| add _ _ _ _ h₁ h₂ =>

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_2.inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊥ ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ ⊥

pp: case refine_2.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ ⊤

Tactic:
· rw [if_neg]
          intro con
          exact bot_ne_top (eq_top_iff.2 (h con))

Goal state after:
case refine_2.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ ⊤
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι
ht : t ⊆ image g s
⊢ ∀ ⦃i : ι⦄, i ∈ image g s → i ∉ t → Disjoint (f i) (t.sup f)

Tactic:
i

Goal state after:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι
ht : t ⊆ image g s
i : ι
⊢ i ∈ image g s → i ∉ t → Disjoint (f i) (t.sup f)
Module: Mathlib.Order.Interval.Set.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a : α
⊢ ⇑e '' Iio a = Iio (e a)

Tactic:
by
  rw [e.image_eq_preimage_symm, e.symm.preimage_Iio, e.symm_symm]

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

Goal state before:
pp: case add
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 x✝ y✝ : A
hx✝ : x✝ ∈ span R s
hy✝ : y✝ ∈ span R s
h₁ : Commute x✝ x
h₂ : Commute y✝ x
⊢ Commute (x✝ + y✝) x

Tactic:
| add _ _ _ _ h₁ h₂ =>

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
this : sSup s = t.sup id
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Tactic:
exact ⟨t, hts, this⟩

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V✝ : Type u_6
S✝ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
x : M
p p' : Submodule R M
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
s✝ t : Set 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
s : ↑S
⊢ ↑s ∈ V

Tactic:
by simpa only [hV] using! subset_span (by simp)

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
M : Type u_4
M₂ : Type u_5
V✝ : Type u_6
S✝ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
x : M
p p' : Submodule R M
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
s✝ t : Set M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
V : Submodule R M
f : ↥V →ₗ[R] N
S : Set M
hV : V = span R S
s : ↑S
⊢ ↑s ∈ V

Tactic:
by simpa only [hV] using! subset_span (by simp)

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

Goal state before:
pp: I : Type u_7
inst✝² : DecidableEq I
M : I → Type u_8
inst✝¹ : (i : I) → CommMonoid (M i)
inst✝ : Fintype I
f : (i : I) → M i
⊢ ∏ i, Pi.mulSingle i (f i) = f

Tactic:
ext a
  simp

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:
by intro x; grind

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

Goal state before:
pp: case inr
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hnk : n < k
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)

Tactic:
← mem_range

Goal state after:
case inr
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hnk : n ∈ range k
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
⊢ optionElim y 0 = single none y

Tactic:
ext a
  cases a
  · simp
  · simp

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : MulZeroOneClass R
s : Set α
r : R
a : α
⊢ r • s.indicator 1 a = s.indicator (fun x ↦ r) a

Tactic:
by
  simp_rw [← indicator_const_smul_apply, Pi.one_apply, smul_eq_mul, mul_one]

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

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
P : Type u_11
inst✝² : AddZeroClass M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
g : N →+ P
f : α → M →+ N
a : α
⊢ liftAddHom.symm (g.comp (liftAddHom f)) a = g.comp (f a)

Tactic:
rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]

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

Goal state before:
pp: case inl
R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
x : R
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
h : v x < 1
⊢ ∃ x, 1 < v x

Tactic:
refine ⟨x⁻¹, ?_⟩
    rw [map_inv₀]
    exact (one_lt_inv₀ <| v.pos hx₀).mpr h

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

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
hf : ∀ x ∈ s, 1 ≤ f x
⊢ 1 < ∏ x ∈ s, f x ↔ ∃ x ∈ s, 1 < f x

Tactic:
have hsum : 1 ≤ ∏ x ∈ s, f x := one_le_prod' hf
  rw [hsum.lt_iff_ne', Ne, prod_eq_one_iff_of_one_le' hf, not_forall]
  simp +contextual [← exists_prop, -exists_const_iff, hf _ _ |>.lt_iff_ne']

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

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    ((False → Disjoint (f z) (f z)) ∧ ∀ a ∈ i, ¬z = a → Disjoint (f z) (f a)) ∧
      ∀ a ∈ i, (¬a = z → Disjoint (f a) (f z)) ∧ ∀ a_2 ∈ i, ¬a = a_2 → Disjoint (f a) (f a_2)

Tactic:
IsEmpty.forall_iff,

Goal state after:
case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (True ∧ ∀ a ∈ i, ¬z = a → Disjoint (f z) (f a)) ∧
      ∀ a ∈ i, (¬a = z → Disjoint (f a) (f z)) ∧ ∀ a_2 ∈ i, ¬a = a_2 → Disjoint (f a) (f a_2)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
h : p
⊢ ∏ᶠ (i : p), f i = f h

Tactic:
have : Unique p := ⟨⟨h⟩, fun _ => rfl⟩

Goal state after:
case pos
M : Type u_2
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
f : p → M
h : p
this : Unique p
⊢ ∏ᶠ (i : p), f i = f h
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ #(Ici a) = n - ↑a

Tactic:
by
  rw [← attachFin_Ico_eq_Ici, card_attachFin, Nat.card_Ico]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∉ s
⊢ ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s ∪ insert a '' 𝒫 s), f t =
    (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) * ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t)

Tactic:
finprod_mem_union (disjoint_powerset_insert has) hs.powerset (hs.powerset.image (insert a)),

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Set α → M
s : Set α
a : α
hs : s.Finite
has : a ∉ s
⊢ (∏ᶠ (i : Set α) (_ : i ∈ 𝒫 s), f i) * ∏ᶠ (i : Set α) (_ : i ∈ insert a '' 𝒫 s), f i =
    (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t) * ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t)
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case inr.inr.inr
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨↑k - 1, ⋯⟩.succ
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) k = vecCons a x ((Equiv.swap i.succ j.succ) k)

Tactic:
Equiv.swap_apply_of_ne_of_ne hki hkj,

Goal state after:
case inr.inr.inr
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨↑k - 1, ⋯⟩.succ
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) k = vecCons a x k
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: y : ℕ∞
h : y ≠ 0
⊢ ⊤ ^ y = ⊤

Tactic:
by
  induction y with
  | top => exact top_epow_top
  | coe y => rwa [epow_natCast, pow_eq_top_iff, eq_self ⊤, true_and, ← y.cast_ne_zero (R := ℕ∞)]

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
z m : ℤ
h : m • p = b - a
⊢ m • z • p = z • b - z • a

Tactic:
← zsmul_sub,

Goal state after:
case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
z m : ℤ
h : m • p = b - a
⊢ m • z • p = z • (b - a)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : SMul G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
w : ι → G
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : ∑ i ∈ s, g₁ i • (w • v) i = ∑ i ∈ s, g₂ i • (w • v) i
⊢ ∀ (i : ι), g₁ i = g₂ i

Tactic:
i

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : SMul G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
w : ι → G
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : ∑ i ∈ s, g₁ i • (w • v) i = ∑ i ∈ s, g₂ i • (w • v) i
i : ι
⊢ g₁ i = g₂ i
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
w : ι → Rˣ
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : ∑ i ∈ s, g₁ i • (w • v) i = ∑ i ∈ s, g₂ i • (w • v) i
⊢ ∀ (i : ι), g₁ i = g₂ i

Tactic:
i

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
w : ι → Rˣ
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : ∑ i ∈ s, g₁ i • (w • v) i = ∑ i ∈ s, g₂ i • (w • v) i
i : ι
⊢ g₁ i = g₂ i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
ih : ∀ i < m ^ n, ∑ x, i / m ^ ↑x % m * m ^ ↑x = i
⊢ ↑⟨∑ i, ↑a / m ^ ↑i % m * m ^ ↑i, ⋯⟩ = ↑a

Tactic:
simp_rw [Fin.sum_univ_succ, Fin.val_zero, Fin.val_succ, pow_zero, Nat.div_one,
          mul_one, pow_succ', ← Nat.div_div_eq_div_mul, mul_left_comm _ m, ← mul_sum]

Goal state after:
case succ
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
ih : ∀ i < m ^ n, ∑ x, i / m ^ ↑x % m * m ^ ↑x = i
⊢ ↑a % m + m * ∑ i, ↑a / m / m ^ ↑i % m * m ^ ↑i = ↑a
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_2
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
⊢ ∀ i ∈ s, g i = 0

Tactic:
i

Goal state after:
case refine_2
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι ⊕ ι'
⊢ i ∈ s → g i = 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
hca : c ∣ a
h : ¬c = 0
⊢ a % c + b % c < c

Tactic:
by
        rw [Nat.mod_eq_zero_of_dvd hca, zero_add]
        exact Nat.mod_lt _ (zero_lt_of_ne_zero h)

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

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
h :
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
t : Finset ι
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i
i : ι
⊢ f i = 0

Tactic:
specialize h t tᶜ f disjoint_compl_right heq
    by_cases hi : i ∈ t
    · exact h.1 i hi
    · exact h.2 i (Finset.mem_compl.2 hi)

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

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ ∑ i ∈ insert a s, g i * i x * i y - ∑ i ∈ insert a s, g i * a x * i y =
    ∑ i ∈ insert a s, g i * (i x * i y) - ∑ i ∈ insert a s, a x * (g i * i y)

Tactic:
congrm ∑ i ∈ insert a s, ?_ - ∑ i ∈ insert a s, ?_
        · rw [mul_assoc]
        · rw [mul_assoc, mul_left_comm]

Goal state after: