mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : ℕ
m : WithBot ℕ∞
⊢ ↑n + ↑↑1 ≤ m ↔ ↑n < m

Tactic:
WithBot.coe_natCast,

Goal state after:
n : ℕ
m : WithBot ℕ∞
⊢ ↑n + ↑1 ≤ m ↔ ↑n < m
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe
n : ℕ
a✝ : ℕ∞
⊢ ↑↑(n + 1) ≤ ↑a✝ ↔ ↑n < ↑a✝

Tactic:
· rw [WithBot.coe_le_coe, natCast_add, natCast_one, ENat.add_one_le_iff (natCast_ne_top n),
      ← WithBot.coe_lt_coe, WithBot.coe_natCast]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (γ × α)
s : Finset γ
t : γ → Finset α
h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1
f : γ × α → β
⊢ ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (c, a)

Tactic:
refine Eq.trans ?_ (prod_sigma s t fun p => f (p.1, p.2))
  apply prod_equiv (Equiv.sigmaEquivProd _ _).symm <;> simp [h]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, p x
⊢ ∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (f x)

Tactic:
simp_rw [apply_ite k]
  exact prod_ite_of_true h _ _

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n.succ → α
⊢ (ofFn f).tail.get = fun i ↦ f i.succ

Tactic:
funext i

Goal state after:
α : Type u_1
n : ℕ
f : Fin n.succ → α
i : Fin (n.succ - 1)
⊢ (ofFn f).tail.get i = f i.succ
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
h : s.Countable
default : α
h_mem : default ∈ s
n : ℕ
⊢ enumerateCountable h default n ∈ s

Tactic:
convert! mem_range_self n
  exact (range_enumerateCountable_of_mem h h_mem).symm

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

Goal state before:
pp: α : Type u_1
n : ℕ
xs : Vector α n
⊢ xs ++ nil = xs

Tactic:
cases xs; simp only [append_def, append_nil]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: case mk.mk
ι : Type u
α : Type v
f : ι → Type v
⊢ (lift.{u, v} #α ^ sum fun i ↦ #(f i)) = prod fun i ↦ #α ^ (fun i ↦ #(f i)) i

Tactic:
simp_rw [← mk_uLift, prod, sum, power_def]

Goal state after:
case mk.mk
ι : Type u
α : Type v
f : ι → Type v
⊢ #((i : ι) × Quotient.out #(f i) → ULift α) = #((i : ι) → Quotient.out #(f i → α))
Module: Mathlib.Order.UpperLower.Basic

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s : Set α
h : IsUpperSet sᶜ
⊢ s = sᶜᶜ

Tactic:
compl_compl

Goal state after:
α : Type u_1
inst✝ : LE α
s : Set α
h : IsUpperSet sᶜ
⊢ s = s
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≺i s
b : β
h : b ∈ {b | s b f.top}
⊢ b ∈ ⇑f.toRelEmbedding '' Set.univ

Tactic:
simpa using mem_range_of_rel_top _ h

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
a b : α
hab : a ≤ b
⊢ IsLeast (Ici a ∩ Ici b) b

Tactic:
inter_eq_self_of_subset_right (Ici_subset_Ici.2 hab)

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
a b : α
hab : a ≤ b
⊢ IsLeast (Ici b) b
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
x : α
⊢ (⨅ i, f i) x = (⨅ i, ⇑(f i)) x

Tactic:
simp [iInf_apply]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: a : Cardinal.{u_1}
⊢ ↑(toNat a) ≤ a

Tactic:
by
  obtain h | h := lt_or_ge a ℵ₀
  · simp [cast_toNat_of_lt_aleph0 h]
  · simp [Cardinal.toNat_apply_of_aleph0_le h]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ lift.{u, v} x ≤ ↑m ↔ x ≤ ↑m

Tactic:
rw [← lift_ofENat.{u, v}, lift_le]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ ↑m ≤ lift.{u, v} x ↔ ↑m ≤ x

Tactic:
rw [← lift_ofENat.{u, v}, lift_le]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Mul N
inst✝⁴ : Mul P
inst✝³ : SMul M N
inst✝² : SMul M P
inst✝¹ : SMulCommClass M N N
inst✝ : SMulCommClass M P P
c : M
x y : N × P
⊢ c • x • y = x • c • y

Tactic:
by simp [smul_def, mul_def, mul_smul_comm]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
m : M
n : N
a : α
⊢ SMul.smul (m, n) a = SMul.smul (m, n) a

Tactic:
change (m, (1 : N)) • ((1 : M), n) • a = _

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
m : M
n : N
a : α
⊢ (m, 1) • (1, n) • a = SMul.smul (m, n) a
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[φ] Y
g : Y → X
k : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : N
x : Y
⊢ g (m • f (g x)) = g (φ (φ' m) • f (g x))

Tactic:
by rw [k]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
x✝ : DistribMulAction (M × N) α
m : M
n : N
a : α
⊢ SMul.smul (m, n) a = SMul.smul (m, n) a

Tactic:
change (m, (1 : N)) • ((1 : M), n) • a = _

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
x✝ : DistribMulAction (M × N) α
m : M
n : N
a : α
⊢ (m, 1) • (1, n) • a = SMul.smul (m, n) a
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case e_4.e_2
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
⊢ (fun x_1 ↦ SMulCommClass M N α) = fun x ↦ SMulCommClass M N α

Tactic:
funext i

Goal state after:
case e_4.e_2
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
i : DistribMulAction N α
⊢ SMulCommClass M N α = SMulCommClass M N α
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case e_4.e_3
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
⊢ compHom α (MonoidHom.inr M N) = x

Tactic:
ext n a; (conv_rhs => rw [← one_smul M (SMul.smul n a)]); rfl

Goal state after:
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 + 1))

Tactic:
by
    rw [iterate_succ]
    exact (iterate_surjective h n).comp h

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : Set M
nonempty : C.Nonempty
linearComb : ∀ x ∈ C, ∀ y ∈ C, ∀ (a b : R), a • x + b • y ∈ C
⊢ 0 ∈ C

Tactic:
by
    obtain ⟨x, hx⟩ := nonempty
    simpa [zero_smul, add_zero] using linearComb x hx x hx 0 0

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q p : Submodule R M
x : M
⊢ x ∈ ⊥ → x ∈ p

Tactic:
by simp +contextual [zero_mem]

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✝ * ↑(Int.negSucc n) = x✝¹ * (x✝ * ↑(Int.negSucc n))

Tactic:
simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev]

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * x✝ * (-1 + -↑n) = x✝¹ * (x✝ * (-1 + -↑n))
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁸ : NonAssocRing R✝
inst✝⁷ : NonAssocRing S✝
inst✝⁶ : NonAssocRing T
s✝ t : Subring R✝
R : Type u
S : Type v
inst✝⁵ : NonAssocSemiring R
inst✝⁴ : NonAssocSemiring S
σR : Type u_1
σS : Type u_2
inst✝³ : SetLike σR R
inst✝² : SetLike σS S
inst✝¹ : SubsemiringClass σR R
inst✝ : SubsemiringClass σS S
e : R ≃+* S
s' : σR
s : σS
h : ∀ (x : R), x ∈ s' ↔ e x ∈ s
y : S
hy : y ∈ s
⊢ ↑e.symm y ∈ s'

Tactic:
by
    obtain ⟨x, rfl⟩ := e.surjective y; simp [(h _).2 hy]

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y * ↑u = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ y * ↑u = A * (B * ↑u)

Tactic:
rw [← mul_assoc, ← HAB]

Goal state after:
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⟩)

Goal state after:
case mpr.inl
M : Type u_2
inst✝ : Monoid M
x y : M
ha : Irreducible x
hb : IsUnit y
⊢ Irreducible (x * y)

case mpr.inr
M : Type u_2
inst✝ : Monoid M
x y : M
hb : Irreducible y
ha : IsUnit x
⊢ Irreducible (x * y)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ Associates.mk a = Associates.mk 1 ↔ a ~ᵤ 1

Tactic:
mk_eq_mk_iff_associated

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ a ~ᵤ 1 ↔ a ~ᵤ 1
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ IsUnit (Associates.mk a) ↔ a ~ᵤ 1

Tactic:
rw [isUnit_iff_eq_one, one_eq_mk_one, mk_eq_mk_iff_associated]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

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

Tactic:
simpa [mem_smul] using! hs

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

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
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
x : M
hx : x ∈ map p.subtype q
⊢ ↥q

Tactic:
refine ⟨⟨x, ?_⟩, ?_⟩ <;> rcases hx with ⟨⟨_, h⟩, _, rfl⟩

Goal state after:
case refine_1
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
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
val✝ : M
h : val✝ ∈ p
left✝ : ⟨val✝, h⟩ ∈ ↑q
⊢ p.subtype ⟨val✝, h⟩ ∈ p

case refine_2
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
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
val✝ : M
h : val✝ ∈ p
left✝ : ⟨val✝, h⟩ ∈ ↑q
⊢ ⟨p.subtype ⟨val✝, h⟩, ⋯⟩ ∈ q
Module: Mathlib.Algebra.Module.Submodule.Equiv

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
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
p : Submodule R N
hf : Injective ⇑f
h : p ≤ f.range
x y : ↥(comap f p)
hxy :
  (LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯) x = (LinearMap.codRestrict p (f ∘ₗ (comap f p).subtype) ⋯) y
⊢ x = y

Tactic:
simpa using hf (Subtype.ext_iff.mp hxy)

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsWeakUpperModularLattice α
a b : α
⊢ a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b

Tactic:
by
  rw [inf_comm, sup_comm]
  exact fun ha hb => covBy_sup_of_inf_covBy_of_inf_covBy_left hb ha

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ Icc (a ⊓ b) b = Icc (b ⊓ a) b

Tactic:
by rw [inf_comm]

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ Ioo (a ⊓ b) b = Ioo (b ⊓ a) b

Tactic:
by rw [inf_comm]

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:
by
  ext x; exact ⟨fun hx ↦ ⟨x, hx.closure_eq⟩, by rintro ⟨y, rfl⟩; exact c.isClosed_closure _⟩

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

Goal state before:
pp: case refine_3
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
⊢ ∃ T, ↑T ⊆ S ∧ x + y ∈ span R ↑T

Tactic:
refine ⟨X ∪ Y, ?_, ?_⟩

Goal state after:
case refine_3.refine_1
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) ⊆ S

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)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb✝ : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := ⋯
u : Finset ι := ⋯
⊢ Disjoint ((t.sup fun i ↦ (g i).sup f) ⊔ u.sup f) (f b)

Tactic:
apply Disjoint.disjoint_sup_left_of_disjoint_sup_right

Goal state after:
case h
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb✝ : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := ⋯
u : Finset ι := ⋯
⊢ Disjoint (u.sup f) (f b)

case hsup
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i ↦ (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
a : Finset ι
ha : a ⊆ s.biUnion g
b : ι
hb✝ : b ∈ s.biUnion g
hab : b ∉ a
i' : ι'
hi' : i' ∈ s
hb : b ∈ g i'
t : Finset ι' := ⋯
u : Finset ι := ⋯
⊢ Disjoint (t.sup fun i ↦ (g i).sup f) (u.sup f ⊔ f b)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep t
hf : Injective f
i : ι'
⊢ ⨆ j, ⨆ (_ : j ≠ i), (t ∘ f) j ≤ ⨆ j, ⨆ (_ : j ≠ f i), t j

Tactic:
refine (iSup_mono fun i => ?_).trans (iSup_comp_le _ f)
    exact iSup_const_mono hf.ne

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

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
h1 : s.mulIndicator f = f
h2 : s ⊆ t
⊢ t.mulIndicator f = f

Tactic:
mulIndicator_eq_self

Goal state after:
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
h1 : mulSupport f ⊆ s
h2 : s ⊆ t
⊢ mulSupport f ⊆ t
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
hs : x ⊓ sSup s = ⊥
⊢ x ≤ sSup s

Tactic:
exact le_sSup hx₀

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

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝³ : FunLike F α α
inst✝² : Monoid F
inst✝¹ : IsOneApplyEqSelf F α
inst✝ : IsMulApplyEqComp F α
f : F
n : ℕ
x : α
⊢ (f ^ n) x = (⇑f)^[n] x

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp [pow_succ', ih, ← Function.iterate_succ_apply']

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
⊢ sSup {c | IsCompactElement c ∧ c ≤ sSup s} = sSup s

Tactic:
exact le_antisymm (sSup_le fun c hc => hc.2) (sSup_le_sSup fun c cs => ⟨hs c cs, le_sSup cs⟩)

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

Goal state before:
pp: case mp.inr.refine_2
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
⊢ a * b = 1

Tactic:
← hb

Goal state after:
case mp.inr.refine_2
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 : b • a • y ≠ 0
⊢ a * b = 1
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i = (g i + h i) * ∏ i ∈ s \ {i}, f i

Tactic:
right_distrib

Goal state after:
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ 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
Module: Mathlib.Algebra.BigOperators.Ring.Finset

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

Tactic:
simp only [prod_attach_univ, prod_sum, Finset.sum_univ_pi]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : Module.End R R
⊢ f (f 1) = f 1 ↔ ∀ (x : R), (f * f) x = f x

Tactic:
Module.End.mul_apply

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : Module.End R R
⊢ f (f 1) = f 1 ↔ ∀ (x : R), f (f x) = f x
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
⊢ ∃ i, a ∈ s i

Tactic:
simpa using ha

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ abv (a * a) = abv a * abv a

Tactic:
abv.map_mul

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ abv a * abv a = abv a * abv a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : α →₀ M
a : α
ha : ¬x a = 0
⊢ ¬(mapDomain (⇑f) x) (f a) = 0

Tactic:
simpa [f.injective]

Goal state after:
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 + h i) * ∏ i ∈ s \ {i}, f i

Tactic:
right_distrib

Goal state after:
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
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
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
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ (g i + h i) * ∏ i ∈ s \ {i}, f i

Tactic:
right_distrib

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
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
⊢ 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
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ {x ∈ s | f x ≠ 1} ⊆ t

Tactic:
simpa only [subset_iff, mem_filter, and_imp]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
αs : ι → Type u_12
inst✝¹ : Zero M
l : (i : ι) × αs i →₀ M
inst✝ : Zero N
g : (i : ι) → (αs i →₀ M) → N
hg : ∀ (i : ι) (x : αs i →₀ M), x = 0 ↔ g i x = 0
i : ι
⊢ i ∈ l.splitSupport ↔ g i (l.split i) ≠ 0

Tactic:
rw [mem_splitSupport_iff_nonzero, not_iff_not, hg]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
l : α' →₀ M
hl : l ∈ supported M R (f '' s)
c : α'
hc : c ∈ l.support
hx : Function.invFunOn f s c ∈ ↑((lmapDomain M R (Function.invFunOn f s)) l).support
⊢ ∃ a ∈ s, f a = c

Tactic:
by simpa using hl hc

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
l : α' →₀ M
hl : l ∈ supported M R (f '' s)
c : α'
hc : c ∈ l.support
⊢ ∃ a ∈ s, f a = c

Tactic:
by simpa using hl hc

Goal state after: