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

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ ↑n * (x✝¹ * x✝) = ↑n * x✝¹ * x✝

Tactic:
(natCast_mem_center _ n).left_assoc _ _

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ ↑n * x✝¹ * x✝ = ↑n * x✝¹ * x✝
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
S T : Subsemigroup M
this : S ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Tactic:
tauto

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
S T : Subsemigroup M
this : T ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
tauto

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

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * (x✝ * ↑n)) = x✝¹ * -(x✝ * ↑n)

Tactic:
mul_neg

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ -(x✝¹ * (x✝ * ↑n)) = -(x✝¹ * (x✝ * ↑n))
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
i : ι
this : S i ≤ iSup S
⊢ ∀ {x : M}, x ∈ S i → x ∈ iSup S

Tactic:
tauto

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
S : Set (Subsemigroup M)
s : Subsemigroup M
hs : s ∈ S
this : s ≤ sSup S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Tactic:
tauto

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

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

Tactic:
mul_neg

Goal state after:
M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ -(x✝¹ * (x✝ * a)) = -(x✝¹ * (x✝ * a))
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝¹ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝ : NonUnitalNonAssocSemiring S
e : R ≃+* S
x✝¹ x✝ : ↥(center R)
⊢ ↑((Subsemigroup.centerCongr ↑e).toFun (x✝¹ + x✝)) =
    ↑((Subsemigroup.centerCongr ↑e).toFun x✝¹ + (Subsemigroup.centerCongr ↑e).toFun x✝)

Tactic:
by exact map_add e ..

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝ : R
⊢ 1 • (algebraMap R A) x✝ = (algebraMap R A) x✝

Tactic:
one_smul

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝ : R
⊢ (algebraMap R A) x✝ = (algebraMap R A) x✝
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
m : M
⊢ (algebraMap R A) r • m = (algebraMap R A) r • 1 • m

Tactic:
one_smul

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
m : M
⊢ (algebraMap R A) r • m = (algebraMap R A) r • m
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case mpr
M : Type u_2
inst✝ : Monoid M
x y : M
⊢ Irreducible x ∧ IsUnit y ∨ Irreducible y ∧ IsUnit x → Irreducible (x * y)

Tactic:
· rintro (⟨ha, hb⟩ | ⟨hb, ha⟩)
    · rwa [irreducible_mul_isUnit hb]
    · rwa [irreducible_isUnit_mul ha]

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

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x y : R
hy : y ∈ s
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ y + (x - y) ∈ closure (↑s ∪ ⇑f ⁻¹' {0})

Tactic:
exact Subring.add_mem _ (subset_closure <| Or.inl hy) (subset_closure <| Or.inr hxy)

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
q r : M
u : Mˣ
h' : q * ↑u ~ᵤ q
hp : q * ↑u ≠ 0
x : M
hx : ¬IsUnit x ∧ r = q * ↑u * x
hq : q ≠ 0
⊢ r = q * ↑u * x

Tactic:
← hx.2

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
q r : M
u : Mˣ
h' : q * ↑u ~ᵤ q
hp : q * ↑u ≠ 0
x : M
hx : ¬IsUnit x ∧ r = q * ↑u * x
hq : q ≠ 0
⊢ r = r
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₂
ι : Type u_1
A : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
i j : ι
h : i = j
x✝ : R
⊢ (RingEquiv.cast h).toFun ((algebraMap R (A i)) x✝) = (algebraMap R (A j)) x✝

Tactic:
cases h

Goal state after:
case refl
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₂
ι : Type u_1
A : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
i : ι
x✝ : R
__spread✝⁻⁰ : A i ≃+* A i := RingEquiv.cast ⋯
⊢ (RingEquiv.cast ⋯).toFun ((algebraMap R (A i)) x✝) = (algebraMap R (A i)) x✝
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Injective ⇑f
y : M
this : ⟨f y, ⋯⟩ = (ofInjective f h) y
⊢ f ((ofInjective f h).symm ⟨f y, ⋯⟩) = ↑⟨f y, ⋯⟩

Tactic:
simp [this]

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

Goal state before:
pp: case zero
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
⊢ a ≤ 1 • a

Tactic:
one_smul

Goal state after:
case zero
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
⊢ a ≤ a
Module: Mathlib.Algebra.Order.Group.Action

Goal state before:
pp: case zero
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
⊢ 1 • a ≤ a

Tactic:
one_smul

Goal state after:
case zero
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
⊢ a ≤ a
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case inr
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✝ ∈ t
hn : n✝ ∈ N
⊢ r✝ • n✝ ∈ s • N ⊔ t • N

Tactic:
exact Submodule.mem_sup_right (mem_set_smul_of_mem_mem hr hn)

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
c : ClosureOperator α
⊢ {x | c.IsClosed x} = range ⇑c

Tactic:
ext x; exact ⟨fun hx ↦ ⟨x, hx.closure_eq⟩, by rintro ⟨y, rfl⟩; exact c.isClosed_closure _⟩

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: case codisjoint
α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
⊢ (b ⊓ a ⊔ c) ⊓ a = a

Tactic:
simp [inf_of_le_left h₂, h₁.sup_eq_top]

Goal state after:
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
p p' : Submodule R M
m : M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = m) ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v

Tactic:
tauto

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

Goal state before:
pp: case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ R ∙ y
⊢ ∀ (a : R), ∀ x ∈ R ∙ y, (∃ a, a • y = x) → ∃ a_2, a_2 • y = a • x

Tactic:
rintro a _ - ⟨b, rfl⟩

Goal state after:
case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ R ∙ y
a b : R
⊢ ∃ a_1, a_1 • y = a • b • y
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝² : PartialOrder α✝
α : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : IsStronglyCoatomic α
⊢ IsStronglyAtomic αᵒᵈ

Tactic:
by
  rwa [isStronglyAtomic_dual_iff_is_stronglyCoatomic]

Goal state after:
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
x : M
⊢ (∀ v ∈ ⊤, ∃ r, r • x = v) ↔ ∀ (v : M), ∃ r, r • x = v

Tactic:
tauto

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
⊢ x + y ∈ span R ↑(X ∪ Y)

Tactic:
rw [Finset.coe_union, span_union, mem_sup]

Goal state after:
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
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : 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
⊢ f '' latticeClosure s = latticeClosure (f '' s)

Tactic:
simp only [subset_antisymm_iff, Set.image_subset_iff]
  constructor <;> apply latticeClosure_sup_inf_induction
  · exact fun a ha ↦ subset_latticeClosure <| Set.mem_image_of_mem _ ha
  · rintro a - b - ha hb
    simpa [map_sup] using isSublattice_latticeClosure.supClosed ha hb
  · rintro a - b - ha hb
    simpa [map_inf] using isSublattice_latticeClosure.infClosed ha hb
  · exact Set.image_mono subset_latticeClosure
  · rintro _ - _ - ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩
    exact ⟨a ⊔ b, isSublattice_latticeClosure.supClosed ha hb, map_sup ..⟩
  · rintro _ - _ - ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩
    exact ⟨a ⊓ b, isSublattice_latticeClosure.infClosed ha hb, map_inf ..⟩

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : s.Finite
⊢ (_root_.latticeClosure s).Finite

Tactic:
rw [← supClosure_infClosure]

Goal state after:
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : s.Finite
⊢ (supClosure (infClosure s)).Finite
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
b c : α
hab : c ≠ b
h : Disjoint c b
⊢ sSup ({c, b} \ {c}) = b

Tactic:
simp [hab, sSup_singleton]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ sSup ({a, c} \ {c}) = a

Tactic:
simp [hab, sSup_singleton]

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

Goal state before:
pp: R : Type u
A : Type w
M : Type v₁
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : MulAction A M
inst✝¹ : SMul R M
inst✝ : IsScalarTower R A M
r : R
x : M
⊢ r • 1 • x = r • x

Tactic:
one_smul

Goal state after:
R : Type u
A : Type w
M : Type v₁
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : MulAction A M
inst✝¹ : SMul R M
inst✝ : IsScalarTower R A M
r : R
x : M
⊢ r • x = r • x
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
x : R
⊢ x • 1 = x • 1 • 1

Tactic:
one_smul

Goal state after:
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : β → α
g : α → M
x : β
⊢ (f ⁻¹' s).mulIndicator (g ∘ f) x = s.mulIndicator g (f x)

Tactic:
tauto

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ s0 • y ∈ span R (s • t)

Tactic:
refine span_induction (fun x hx ↦ subset_span <| by exact ⟨x, hx, y, hy, rfl⟩) ?_ ?_ ?_
        (hs ▸ mem_top : s0 ∈ span R s)

Goal state after:
case refine_1
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ 0 • y ∈ span R (s • t)

case refine_2
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ ∀ (x y_1 : S),
    x ∈ span R s → y_1 ∈ span R s → x • y ∈ span R (s • t) → y_1 • y ∈ span R (s • t) → (x + y_1) • y ∈ span R (s • t)

case refine_3
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ ∀ (a : R), ∀ x ∈ span R s, x • y ∈ span R (s • t) → (a • x) • y ∈ span R (s • t)
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ ∏ x ∈ s, f x = 0 ↔ ∃ a ∈ s, f a = 0

Tactic:
classical
    induction s using Finset.induction_on with
    | empty => exact ⟨Not.elim one_ne_zero, fun ⟨_, H, _⟩ => by simp at H⟩
    | insert _ _ ha ih => rw [prod_insert ha, mul_eq_zero, exists_mem_insert, ih]

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

Goal state before:
pp: case mp.inr.refine_1
R : Type u_8
M : Type u_9
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ b * a = 1

Tactic:
apply smul_left_injective R hy

Goal state after:
case mp.inr.refine_1
R : Type u_8
M : Type u_9
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ (fun x ↦ x • y) (b * a) = (fun x ↦ x • y) 1
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : CommSemiring R
s : Finset ι
f : ι → Set κ
g : ι → κ → R
⊢ ∏ i ∈ s, (f i).indicator (g i) = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i)

Tactic:
by
  ext a; simpa using prod_indicator_apply ..

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
⊢ Disjoint (⨆ i ∈ s, f i) a

Tactic:
by
  simp_rw [disjoint_iff, iSup_subtype', ← sSup_range, inf_comm, inf_sSup_eq_iSup_inf_sup_finset,
    iSup_eq_bot]
  intro u hu
  obtain ⟨t, ht, ht', htu⟩ : ∃ᵉ (t ⊆ s) (hu : t.Finite), f '' t = u :=
    Set.Finite.exists_subset_finite_image_eq u.finite_toSet <| by rwa [Set.image_eq_range f s]
  replace htu : u.sup id = ⨆ i ∈ t, f i := by
    simp only [Finset.sup_eq_iSup, id_eq, ← Finset.mem_coe, ← htu, iSup_image]
  rw [inf_comm, ← disjoint_iff, htu]
  exact hs t ht ht'

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

Goal state before:
pp: case inr.refine_2
α : Type u_2
inst✝ : CompleteLattice α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
a : α
ba : b ≤ a
h : Maximal (fun x ↦ x ∈ Iio k) a
⊢ ∃ a, IsCoatom a ∧ ⟨b, hbk⟩ ≤ a

Tactic:
refine ⟨⟨a, le_of_lt h.prop⟩, ⟨ne_of_lt h.prop, fun c hck => by_contradiction fun c₀ => ?_⟩, ba⟩
    cases h.eq_of_le (y := c.1) (lt_of_le_of_ne c.2 fun con ↦ c₀ (Subtype.ext con)) hck.le
    exact lt_irrefl _ hck

Goal state after:
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: case cons
α : Type u_1
t : Multiset α
a : α
s : Multiset α
ih : (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal
⊢ map (fun x ↦ Prod.map id (cons a) x)
        (s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal) +
      map (fun x ↦ Prod.map (cons a) id x)
        (s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal) =
    (s.antidiagonal.bind fun a_1 ↦
        map (fun q ↦ ((Prod.map id (cons a) a_1).1 + q.1, (Prod.map id (cons a) a_1).2 + q.2)) t.antidiagonal) +
      s.antidiagonal.bind fun a_1 ↦
        map (fun q ↦ ((Prod.map (cons a) id a_1).1 + q.1, (Prod.map (cons a) id a_1).2 + q.2)) t.antidiagonal

Tactic:
map_bind,

Goal state after:
case cons
α : Type u_1
t : Multiset α
a : α
s : Multiset α
ih : (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal
⊢ ((s.antidiagonal.bind fun a_1 ↦
        map (fun x ↦ Prod.map id (cons a) x) (map (fun q ↦ (a_1.1 + q.1, a_1.2 + q.2)) t.antidiagonal)) +
      s.antidiagonal.bind fun a_1 ↦
        map (fun x ↦ Prod.map (cons a) id x) (map (fun q ↦ (a_1.1 + q.1, a_1.2 + q.2)) t.antidiagonal)) =
    (s.antidiagonal.bind fun a_1 ↦
        map (fun q ↦ ((Prod.map id (cons a) a_1).1 + q.1, (Prod.map id (cons a) a_1).2 + q.2)) t.antidiagonal) +
      s.antidiagonal.bind fun a_1 ↦
        map (fun q ↦ ((Prod.map (cons a) id a_1).1 + q.1, (Prod.map (cons a) id a_1).2 + q.2)) t.antidiagonal
Module: Mathlib.Data.Multiset.Sections

Goal state before:
pp: α : Type u_1
s : Multiset (Multiset α)
⊢ ∀ {a : Multiset α}, a ∈ s.Sections ↔ Rel (fun s a ↦ a ∈ s) s a

Tactic:
induction s using Multiset.induction_on with
  | empty => simp
  | cons _ _ ih => simp [ih, rel_cons_left, eq_comm]

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c✝ : α
hbc : b ≤ c✝
h : sSup {a | a ≤ c✝ ∧ IsAtom a} = c✝
c : Set (Set α)
hc1 : c ⊆ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c✝}
hc2 : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (sSup '' c)

Tactic:
rw [directedOn_image]
      exact hc2.directedOn.mono @fun s t => sSup_le_sSup

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

Goal state before:
pp: case neg
α : Type u_1
M : Type u_4
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise f g x

Tactic:
· rw [piecewise_eq_of_notMem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_notMem h,
      Set.mulIndicator_of_mem (Set.mem_compl h), one_mul]

Goal state after:
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✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
p : Submodule R₂ M₂
⊢ IsCoatom (comap f p) ↔ IsCoatom p

Tactic:
have := comap_injective_of_surjective hf

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective ⇑f
p : Submodule R₂ M₂
this : Injective (comap f)
⊢ IsCoatom (comap f p) ↔ IsCoatom p
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ a a_1 h ∈ {False}) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1

Tactic:
tauto

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
⊢ ∀ a ⊆ s, ∀ (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) ↔ a_1 ∈ a

Tactic:
tauto

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

Goal state before:
pp: case e_a.e_s
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
f g : ι → R
s : Finset ι
a : (a : ι) → a ∈ s → Prop
x✝ : a ∈ s.pi fun x ↦ {True, False}
x : ι
⊢ x ∈ s → ((∃ (h : x ∈ s), ¬a x ⋯) ↔ x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1)

Tactic:
tauto

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
f : α → M
⊢ {a}.indicator f = ⇑(single a (f a))

Tactic:
by
  classical rw [Set.indicator_singleton, single_eq_pi_single]

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

Goal state before:
pp: case neg
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f✝ : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
b : F
h : b ∉ Set.range ⇑f
⊢ (embDomain f (v + w)) b = (embDomain f v + embDomain f w) b

Tactic:
· simp only [coe_add, Pi.add_apply, embDomain_of_notMem_range _ _ _ h, add_zero]

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

Goal state before:
pp: case mpr
α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
⊢ f ≠ 0 ∨ y ≠ 0 → optionElim y f ≠ 0

Tactic:
· intro h
    cases h with
    | inl h => exact optionElim_ne_zero_of_right y f h
    | inr h => exact optionElim_ne_zero_of_left y f h

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

Goal state before:
pp: case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : i ∈ s
h✝ : ¬j ∈ t
⊢ 1 = 0

Tactic:
tauto

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

Goal state before:
pp: case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : ¬i ∈ s
h✝ : j ∈ t
⊢ 1 = 0

Tactic:
tauto

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

Goal state before:
pp: case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : ¬i ∈ s
h✝ : ¬j ∈ t
⊢ 1 = 0

Tactic:
tauto

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

Goal state before:
pp: case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h✝¹ : i ∈ s
h✝ : j ∈ t
⊢ 0 = 1

Tactic:
tauto

Goal state after: