mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Surjective ⇑f'
n : ℕ
⊢ Surjective ⇑((f' ^ n) ∘ₗ f')

Tactic:
exact (iterate_surjective h n).comp h

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ MulAction.stabilizerSubmonoid R m = MulAction.stabilizerSubmonoid R ↑m

Tactic:
by
  ext
  simp only [MulAction.mem_stabilizerSubmonoid_iff, ← SubMulAction.val_smul, SetLike.coe_eq_coe]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ x ∈ p, f x ∈ q
⊢ (f.restrict hf).ker = comap p.subtype f.ker

Tactic:
restrict_eq_codRestrict_domRestrict,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ x ∈ p, f x ∈ q
⊢ (codRestrict q (f.domRestrict p) ⋯).ker = comap p.subtype f.ker
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:
by
      intros
      simp only [coe_add, map_add, Equiv.toFun_as_coe, Equiv.Set.image_apply]
      rfl

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

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h : ↑n * (a - b) = 0
⊢ n = 0 ∨ a = b

Tactic:
mul_eq_zero,

Goal state after:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
n : ℕ
a b : R
h : ↑n = 0 ∨ a - b = 0
⊢ n = 0 ∨ a = b
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
sg : Subsemigroup R
hg : ↑sg = s
sa : AddSubmonoid R
ha : ↑sa = s
⊢ ∀ {a b : R}, a ∈ s → b ∈ s → a + b ∈ s

Tactic:
subst ha

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
sg : Subsemigroup R
sa : AddSubmonoid R
hg : ↑sg = ↑sa
⊢ ∀ {a b : R}, a ∈ ↑sa → b ∈ ↑sa → a + b ∈ ↑sa
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
sg : Subsemigroup R
hg : ↑sg = s
sa : AddSubmonoid R
ha : ↑sa = s
⊢ 0 ∈ s

Tactic:
subst ha

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
sg : Subsemigroup R
sa : AddSubmonoid R
hg : ↑sg = ↑sa
⊢ 0 ∈ ↑sa
Module: Mathlib.Algebra.Module.Submodule.Map

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₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₂₁ : R₂ →+* R
inst✝ : RingHomSurjective σ₂₁
p : Submodule R₂ M₂
q : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
h : ∀ x ∈ p, f x ∈ q
p' : Submodule R₂ ↥p
⊢ map (f.restrict h) p' = comap q.subtype (map f (map p.subtype p'))

Tactic:
restrict_eq_codRestrict_domRestrict,

Goal state after:
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₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₂₁ : R₂ →+* R
inst✝ : RingHomSurjective σ₂₁
p : Submodule R₂ M₂
q : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
h : ∀ x ∈ p, f x ∈ q
p' : Submodule R₂ ↥p
⊢ map (codRestrict q (f.domRestrict p) ⋯) p' = comap q.subtype (map f (map p.subtype p'))
Module: Mathlib.Algebra.Module.Submodule.Map

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₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₂₁ : R₂ →+* R
p : Submodule R₂ M₂
q : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
h : ∀ x ∈ p, f x ∈ q
p' : Submodule R ↥q
⊢ comap (f.restrict h) p' = comap p.subtype (comap f (map q.subtype p'))

Tactic:
restrict_eq_codRestrict_domRestrict,

Goal state after:
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₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₂₁ : R₂ →+* R
p : Submodule R₂ M₂
q : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
h : ∀ x ∈ p, f x ∈ q
p' : Submodule R ↥q
⊢ comap (codRestrict q (f.domRestrict p) ⋯) p' = comap p.subtype (comap f (map q.subtype p'))
Module: Mathlib.Algebra.Ring.Submonoid.Basic

Goal state before:
pp: case mem
M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
ha : a ∈ closure ↑S
r : R
hr : r ∈ ↑S
⊢ a * r ∈ closure ↑S

Tactic:
exact MulMemClass.mul_right_mem_add_closure ha hr

Goal state after:
Module: Mathlib.Algebra.Prime.Defs

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
h : p ∣ a ^ n
⊢ p ∣ a

Tactic:
induction n with
  | zero =>
    rw [pow_zero] at h
    have := isUnit_of_dvd_one h
    have := not_isUnit hp
    contradiction
  | succ n ih =>
    rw [pow_succ'] at h
    rcases dvd_or_dvd hp h with dvd_a | dvd_pow
    · assumption
    · exact ih dvd_pow

Goal state after:
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:
HP,

Goal state after:
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 * -L.prod = -(hd * L.prod)
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 = -1
⊢ -1 * tl.prod = L.prod

Tactic:
HP,

Goal state after:
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 = -1
⊢ -1 * -L.prod = L.prod
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∃ c, b = a * c) → ∃ x, a * x ~ᵤ b

Tactic:
rintro ⟨c, rfl⟩
    use c

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₂
r : R
⊢ e.toRingEquiv.symm.toFun ((algebraMap R A₂) r) = (algebraMap R A₁) r

Tactic:
rw [← e.toRingEquiv.symm_apply_apply (algebraMap R A₁ r)]
      congr
      simp

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₂'
⊢ (fun ψ ↦ e.symm.trans (ψ.trans e')) ((fun ψ ↦ e.trans (ψ.trans e'.symm)) ψ) = ψ

Tactic:
by
    ext
    simp_rw [trans_apply, apply_symm_apply]

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N₁ N₂ N : Submodule R M
h₁ : N₁ ≤ N
h₂ : N₂ ≤ N
⊢ map N.subtype ((N₁ ⊔ N₂).submoduleOf N) = map N.subtype (N₁.submoduleOf N ⊔ N₂.submoduleOf N)

Tactic:
simp only [submoduleOf, map_comap_eq]

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N₁ N₂ N : Submodule R M
h₁ : N₁ ≤ N
h₂ : N₂ ≤ N
⊢ N.subtype.range ⊓ (N₁ ⊔ N₂) = map N.subtype (comap N.subtype N₁ ⊔ comap N.subtype N₂)
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 (Submodule R M)
⊢ span R (⋂ S ∈ s, ↑S) = sInf s

Tactic:
← Submodule.coe_sInf,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
⊢ span R ↑(sInf s) = sInf s
Module: Mathlib.Order.SupClosed

Goal state before:
pp: ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s t : Set α
a b : α
⊢ ∀ (x : Set α), SupClosed {a | ∃ t, ∃ (ht : t.Nonempty), ↑t ⊆ x ∧ t.sup' ht id = a}

Tactic:
rintro s _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩

Goal state after:
ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s✝ t✝ : Set α
a b : α
s : Set α
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ t.sup' ht id ⊔ u.sup' hu id ∈ {a | ∃ t, ∃ (ht : t.Nonempty), ↑t ⊆ s ∧ t.sup' ht id = a}
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
a : α
b : ↑(Ici a)
⊢ IsAtom b ↔ a ⋖ ↑b

Tactic:
rw [← bot_covBy_iff]
  refine (Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => a ≤ c) ?_).symm
  simpa only [OrderEmbedding.coe_subtype, Subtype.range_coe_subtype] using! Set.ordConnected_Ici

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 : Submodule R M
⊢ IsPrincipal R ↥p ↔ p.IsPrincipal

Tactic:
IsPrincipal,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ⊤.IsPrincipal ↔ p.IsPrincipal
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : M
ha : p = R ∙ a
⊢ ∃ a, ⊤ = R ∙ a

Tactic:
refine ⟨⟨a, ha ▸ mem_span_singleton_self a⟩, .symm <| top_unique fun x _ ↦ ?_⟩
    have ⟨r, hr⟩ := mem_span_singleton.mp (ha.le x.2)
    exact mem_span_singleton.mpr ⟨r, Subtype.ext hr⟩

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
⊢ Finset.univ.sup f = f 0 ⊔ f 1 ⊔ f 2

Tactic:
show (Finset.univ : Finset (Fin 3)) = {0, 1, 2} from rfl

Goal state after:
α : Type u_5
inst✝ : CompleteLattice α
f : Fin 3 → α
⊢ {0, 1, 2}.sup f = f 0 ⊔ f 1 ⊔ f 2
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
h_1 : x ∈ s
⊢ f x = g x

Tactic:
exact h h_1

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
this : (s \ ↑(insert ⊥ t)).Infinite
x : α
hx₁ : x ∈ s
hx₂ : x ∉ ↑(insert ⊥ t)
⊢ x ≠ ⊥ ∧ x ∉ t

Tactic:
by simpa [not_or] using hx₂

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

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

Tactic:
mul_eq_zero,

Goal state after:
case insert
ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a✝ : ι
s✝ : Finset ι
ha : a✝ ∉ s✝
ih : ∏ x ∈ s✝, f x = 0 ↔ ∃ a ∈ s✝, f a = 0
⊢ f a✝ = 0 ∨ ∏ x ∈ s✝, f x = 0 ↔ ∃ a ∈ insert a✝ s✝, f a = 0
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : IsCompactElement c
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id

Tactic:
CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : ∀ (s : Set α), c ≤ sSup s → ∃ t, ↑t ⊆ s ∧ c ≤ t.sup id
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i}
⊢ Disjoint (f i) (s.sup id)

Tactic:
rw [← Finset.sup_erase_bot]
  set t := s.erase ⊥
  replace hf : InjOn f (f ⁻¹' t) := fun i hi j _ hij ↦ by
    refine hf ?_ ?_ hij <;> aesop (add norm simp [t])
  have : (Finset.erase (insert i (t.preimage _ hf)) i).image f = t := by
    ext a
    simp only [Finset.mem_preimage, Finset.mem_erase, ne_eq,
      Finset.erase_insert_eq_erase, Finset.mem_image, t]
    refine ⟨by aesop, fun ⟨ha, has⟩ ↦ ?_⟩
    obtain ⟨j, hj, rfl⟩ := hs has
    exact ⟨j, ⟨hj, ha, has⟩, rfl⟩
  rw [← this, Finset.sup_image]
  specialize h (insert i (t.preimage _ hf))
  rw [Finset.supIndep_iff_disjoint_erase] at h
  exact h i (Finset.mem_insert_self i _)

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

Goal state before:
pp: M₀ : Type u_4
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a : M₀
l : List M₀
⊢ a * l.prod = 0 ↔ 0 ∈ a :: l

Tactic:
mul_eq_zero,

Goal state after:
M₀ : Type u_4
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
a : M₀
l : List M₀
⊢ a = 0 ∨ l.prod = 0 ↔ 0 ∈ a :: l
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
⊢ (a ::ₘ s + t).antidiagonal = (a ::ₘ s).antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal

Tactic:
| cons a s ih =>

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

Goal state before:
pp: case cons
α : Type u_1
a : α
s : Multiset α
ih : map Prod.swap s.antidiagonal = s.antidiagonal
⊢ map Prod.swap (a ::ₘ s).antidiagonal = (a ::ₘ s).antidiagonal

Tactic:
| cons a s ih =>

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₂
p : Submodule R M
x y : M
hy : y ∈ ↑p
e : f y = f x
⊢ x - y ∈ f.ker

Tactic:
by simpa using sub_eq_zero.2 e.symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : One β
s : γ → Set α
f : α → β
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
i : α
j : γ
hj✝ : i ∈ s j
j' : γ
h : j' ≠ j
hj : {i} ⊆ s j
⊢ {i} ⊆ s j' → {i} ⊆ mulSupport f → False

Tactic:
hj'

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : One β
s : γ → Set α
f : α → β
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
i : α
j : γ
hj✝ : i ∈ s j
j' : γ
h : j' ≠ j
hj : {i} ⊆ s j
hj' : {i} ⊆ s j'
⊢ {i} ⊆ mulSupport f → False
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
hp : {x | x ∈ s ∧ p x}.Subsingleton
⊢ find? p s hp = some a → p a

Tactic:
by
  induction s using Quotient.inductionOn with | _ l
  simp only [quot_mk_to_coe, find?_coe _ _ hp]
  simpa using l.find?_some  (p := (p ·))

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
g : ι → α
⊢ ⇑(indicator s fun i x ↦ g i) = (↑s).indicator g

Tactic:
by
  classical
  ext i
  simp [indicator_apply, Set.indicator_apply]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ motive f

Tactic:
suffices motive (single a (f a) + f.erase a) by rwa [single_add_erase] at this
    classical
      apply single_add
      · rw [support_erase, mem_erase]
        exact fun H => H.1 rfl
      · rw [← mem_support_iff, hf]
        exact mem_cons_self _ _
      · apply ih _ _
        rw [support_erase, hf, Finset.erase_cons]

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

Goal state before:
pp: case refine_3
ι : Type u_1
R : Type u_2
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
⊢ 0 ≤ g i

Tactic:
exact (hf i hi).le.trans hilt.le

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_3
s : Multiset ι
hs : s ≠ 0
f g : ι → R
h0 : ∀ (i : ι), i ∈ s → 0 < f i
h : ∀ (i : ι), i ∈ s → f i < g i
⊢ (map f s).prod < (map g s).prod

Tactic:
by
  cases s using Quotient.ind
  simp only [quot_mk_to_coe, mem_coe, map_coe, prod_coe, ne_eq, coe_eq_zero] at *
  apply List.prod_map_lt_prod_map hs f g h0 h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
h : x = 0
⊢ mapDomain f x = 0

Tactic:
rw [h, mapDomain_zero]

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

Goal state before:
pp: case neg
α : Type u_2
s : Finset α
f : α → ℕ
h : ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1
hx : ∀ x ∈ s, f x = 0
⊢ ∑ x ∈ s, f x ≤ 1

Tactic:
· simp [sum_congr rfl hx]

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)
this : ∀ x ∈ i, x ≠ z
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔ (Disjoint (f z) (i.sum f) ∧ Disjoint (f z) (i.sum f)) ∧ i.sum f = i.sup f

Tactic:
and_self_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)
this : ∀ x ∈ i, x ≠ z
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔ Disjoint (f z) (i.sum f) ∧ i.sum f = i.sup f
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✝ : Fintype ι
b : Basis ι R M
x : ι → R
⊢ b.equivFun.symm x = ∑ i, x i • b i

Tactic:
simp [Basis.equivFun, Finsupp.linearCombination_apply, sum_fintype, equivFunOnFinite]

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

Goal state before:
pp: case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
z : α →₀ R
hz : z ∈ supported R R s
c : α
this : DecidablePred fun x ↦ x ∈ s
h : c ∈ s
⊢ z c • v c ∈ span R (v '' s)

Tactic:
exact smul_mem _ _ (subset_span (Set.mem_image_of_mem _ h))

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

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun x ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
⊢ (b.repr x) i = f x i

Tactic:
have : Finsupp.lapply i ∘ₗ ↑b.repr = f_i := by
    refine b.ext fun j => ?_
    change b.repr (b j) i = f (b j) i
    rw [b.repr_self, f_eq]

Goal state after:
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun x ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
this : lapply i ∘ₗ ↑b.repr = f_i
⊢ (b.repr x) i = f x i
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
x : M
i : ι
h : b i ∈ Finset.image (⇑b) Finset.univ
⊢ (b.reindexFinsetRange.repr x) ⟨b i, h⟩ = (b.repr x) i

Tactic:
simp [reindexFinsetRange]

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

Goal state before:
pp: case neg
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : ¬↑i + ↑i < n
⊢ ↑i + ↑i - n = (↑i + ↑i) % n

Tactic:
rw [Fin.val_mk, not_lt] at h

Goal state after:
case neg
α : Type u
n : ℕ
v : Fin n → α
i : Fin n
h : n ≤ ↑i + ↑i
⊢ ↑i + ↑i - n = (↑i + ↑i) % n
Module: Mathlib.Order.Interval.Finset.Fin

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

Tactic:
Nat.card_Ioo,

Goal state after:
n : ℕ
a : Fin n
⊢ n - ↑a - 1 = n - 1 - ↑a