mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ x * 1 = x

Tactic:
rw [mul_def, one_def, lift_apply_of]

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ (lift fun x₁ ↦ of (x₁ * 1)) x = x
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : M
h : f x = f y
⊢ g x = g y

Tactic:
obtain ⟨c, hc⟩ := f.eq_iff_exists.1 h
  rw [← one_mul (g x), ← IsUnit.liftRight_inv_mul (g.domRestrict S) hg c]
  change _ * g c * _ = _
  rw [mul_assoc, ← g.map_mul, hc, mul_comm, mul_inv_left hg, g.map_mul]

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
⊢ r₃ * v * ↑s₂ = r₃ * (↑u * r₁)

Tactic:
rw [mul_assoc, ← huv]

Goal state after:
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a b : WithZero G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun a ≤ (MulEquiv.withZero e.toMulEquiv).toFun b ↔ a ≤ b

Tactic:
cases a <;> cases b <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
⊢ succ a = sInf (Ioi a)

Tactic:
by
  apply (le_csInf nonempty_Ioi fun b => succ_le_of_lt).antisymm
  exact csInf_le ⟨a, fun b => le_of_lt⟩ <| lt_succ a

Goal state after:
Module: Mathlib.Data.Fintype.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ s.powerset = univ.powerset ↔ s = univ

Tactic:
powerset_inj

Goal state after:
α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ s = univ ↔ s = univ
Module: Mathlib.Data.Fintype.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
k : ℕ
⊢ card { s // #s = k } = (card α).choose k

Tactic:
by
  simp [Fintype.subtype_card, Finset.card_univ]

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:

Tactic:
_ = ∏ j, #(Function.update s i {a} j) := by
      rw [← piFinset_update_singleton_eq_filter_piFinset_eq _ _ ha, Fintype.card_piFinset]
    _ = ∏ j, Function.update (fun j ↦ #(s j)) i 1 j :=
      Fintype.prod_congr _ _ fun j ↦ by obtain rfl | hji := eq_or_ne j i <;> simp [*]
    _ = _ := by simp [prod_update_of_mem, erase_eq]

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

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
a✝ a : α
i : Fin (n + 1)
v : Vector α n
⊢ ((↑v).insertIdx (↑i) a).length = n + 1

Tactic:
List.length_insertIdx,

Goal state after:
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
a✝ a : α
i : Fin (n + 1)
v : Vector α n
⊢ (if ↑i ≤ (↑v).length then (↑v).length + 1 else (↑v).length) = n + 1
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : x ≤ y
⊢ (sumLexIioIci x).symm y = toLex (Sum.inr ⟨y, h⟩)

Tactic:
by
  rw [symm_apply_eq, sumLexIioIci_apply_inr]

Goal state after:
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : SuccOrder α
x : α
⊢ ⨆ a, succ ↑a = x

Tactic:
have H : BddAbove (range fun a : Iio x ↦ succ a.1) :=
    ⟨succ x, by simp +contextual [upperBounds, succ_le_succ, le_of_lt]⟩
  apply le_antisymm _ (le_of_forall_lt fun y hy ↦ ?_)
  · rw [ciSup_le_iff' H]
    exact fun a ↦ succ_le_of_lt a.2
  · rw [lt_ciSup_iff' H]
    exact ⟨⟨y, hy⟩, lt_succ_of_not_isMax hy.not_isMax⟩

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : β
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr b) ↔ inr a ≤ inr b

Tactic:
change inr (toDual a) ≤ inr (toDual b) ↔ toDual (inr a) ≤ toDual (inr b)
        simp [toDual_le_toDual, inr_le_inr_iff]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
r : α → α → Prop
β : Type u
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
⊢ ∃ γ t, IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s)

Tactic:
classical
  obtain f | f := f.principalSumRelIso
  · exact ⟨_, _, inferInstance,
      ⟨(RelIso.sumLexCongr f.subrelIso.symm (.refl _)).trans <| .sumLexComplLeft ..⟩⟩
  · exact ⟨PEmpty, nofun, inferInstance, ⟨(RelIso.sumLexEmpty r _).trans f⟩⟩

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ (fun x ↦ (f x, g x)) a ∈ upperBounds ((fun x ↦ (f x, g x)) '' d) ∧
    (fun x ↦ (f x, g x)) a ∈ lowerBounds (upperBounds ((fun x ↦ (f x, g x)) '' d))

Tactic:
upperBounds

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ (fun x ↦ (f x, g x)) a ∈ {x | ∀ ⦃a : β × γ⦄, a ∈ (fun x ↦ (f x, g x)) '' d → a ≤ x} ∧
    (fun x ↦ (f x, g x)) a ∈ lowerBounds {x | ∀ ⦃a : β × γ⦄, a ∈ (fun x ↦ (f x, g x)) '' d → a ≤ x}
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case right.left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ (p₁, p₂).1 ∈ upperBounds (f '' d)

Tactic:
upperBounds

Goal state after:
case right.left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ (p₁, p₂).1 ∈ {x | ∀ ⦃a : β⦄, a ∈ f '' d → a ≤ x}
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case right.right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ (p₁, p₂).2 ∈ upperBounds (g '' d)

Tactic:
upperBounds

Goal state after:
case right.right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ (p₁, p₂).2 ∈ {x | ∀ ⦃a : γ⦄, a ∈ g '' d → a ≤ x}
Module: Mathlib.Data.Part

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : ¬o.Dom
⊢ (o.bind f).toOption = Option.none.elim Option.none fun a ↦ (f a).toOption

Tactic:
exact Part.toOption_eq_none_iff.2 fun ho => h ho.of_bind

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map f o = o

Tactic:
rw [show f = id from funext H]; exact id_map o

Goal state after:
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ c₁ ∨ c₁ ⊆ c₂

Tactic:
induction hc₁ with
  | @succ c₃ hc₃ ih =>
    obtain ih | ih := ih
    · exact Or.inl (ih.trans subset_succChain)
    · exact (h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl
  | union _ ih =>
    refine or_iff_not_imp_left.2 fun hn => sUnion_subset fun a ha => ?_
    exact (ih a ha).resolve_left fun h => hn <| h.trans <| subset_sUnion_of_mem ha

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ {y | IsExtremePt x f y}
z : α
hz : z ∈ bot x f
hzy : z < f y
left✝ : z ∈ bot x f
hz' : f y ≤ z
⊢ f z ≤ f y

Tactic:
exfalso
      exact lt_irrefl z (lt_of_lt_of_le hzy hz')

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

Goal state before:
pp: α β : Type u
⊢ Cardinal.{u} ≤i Cardinal.{max u v}

Tactic:
refine ⟨(OrderEmbedding.ofMapLEIff lift ?_).ltEmbedding, ?_⟩

Goal state after:
case refine_1
α β : Type u
⊢ ∀ (a b : Cardinal.{u}), lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b

case refine_2
α β : Type u
⊢ ∀ (a : Cardinal.{u}),
    ∀ b < (OrderEmbedding.ofMapLEIff lift.{v, u} ?refine_1).ltEmbedding a,
      b ∈ Set.range ⇑(OrderEmbedding.ofMapLEIff lift.{v, u} ?refine_1).ltEmbedding
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u
hι : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (Set.range f)
c : Cardinal.{v}
hc : ¬IsSuccLimit c
h : ⨆ i, f i = c
⊢ ∃ i, f i = c

Tactic:
subst h
  exact exists_eq_ciSup_of_not_isSuccLimit hf hc

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

Goal state before:
pp: c : Cardinal.{u}
c' : ℕ
⊢ toENat c ≤ ↑c' ↔ c ≤ ↑c'

Tactic:
← toENat_le_natCast

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

Goal state before:
pp: s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ lift.{u, u_1} (sSup s) = sSup (lift.{u, u_1} '' s)

Tactic:
apply ((le_csSup_iff' (bddAbove_image.{_, u} _ hs)).2 fun c hc => _).antisymm (csSup_le' _)

Goal state after:
s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ ∀ c ∈ upperBounds (lift.{u, u_1} '' s), lift.{u, u_1} (sSup s) ≤ c

s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ lift.{u, u_1} (sSup s) ∈ upperBounds (lift.{u, u_1} '' s)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
h : IsSuccLimit (↑n + 1)
⊢ False

Tactic:
← succ_natCast

Goal state after:
n : ℕ
h : IsSuccLimit (succ ↑n)
⊢ False
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : ∀ (x y : ↥p), x = y
x : M
hx : x ∈ p
⊢ x = 0

Tactic:
by simpa using h ⟨x, hx⟩ ⟨0, p.zero_mem⟩

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✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ Disjoint p f.ker ↔ Set.InjOn ⇑f ↑p

Tactic:
by
  rw [disjoint_ker, Set.injOn_iff_map_eq_zero]

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

Goal state before:
pp: case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
⊢ 0 * ↑u = ↑u * 0

pp: case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
ha : a ≠ 0
⊢ a * ↑u = ↑u * a

Tactic:
· rw [zero_mul, mul_zero]

Goal state after:
case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
ha : a ≠ 0
⊢ a * ↑u = ↑u * a
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
M' : Subsemigroup M
⊢ Function.Surjective ⇑(f.subsemigroupMap M')

Tactic:
rintro ⟨_, x, hx, rfl⟩
  exact ⟨⟨x, hx⟩, rfl⟩

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ AddSubmonoid.closure ↑M
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M

Tactic:
induction hx using AddSubmonoid.closure_induction <;> aesop

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

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

Tactic:
by
        rw [List.map_append, List.sum_append, HL2, HM2]

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⦄, ↑u * y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ IsUnit A ∨ IsUnit B

Tactic:
rw [← u.isUnit_units_mul]
    apply h
    rw [mul_assoc, ← HAB]

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

Goal state before:
pp: M₀✝ : ?m.1
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ ∀ (a : M₀), a ∈ M₀⁰ ↔ ⟦a⟧ ∈ (Quotient (Associated.setoid M₀))⁰

Tactic:
simp [mem_nonZeroDivisors_iff, Quotient.forall, Associates.mk_mul_mk]

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₂
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
f : (S →ₐ[R] S)ˣ
x : S
⊢ ↑(f * f⁻¹) x = x

Tactic:
rw [mul_inv_cancel]; rfl

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : y ≤ x ⊔ z
⊢ x = y

Tactic:
refine hxy.antisymm ?_
  rw [← inf_eq_right, sup_inf_assoc_of_le _ hxy] at hsup
  rwa [← hsup, sup_le_iff, and_iff_right rfl.le, inf_comm]

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder β
inst✝ : Preorder γ
h₁ : WellFoundedLT β
h₂ : WellFoundedLT γ
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
⊢ (fun A ↦ (f₂ A, g₂ A)) A < (fun A ↦ (f₂ A, g₂ A)) B

Tactic:
by
    simp only [Prod.le_def, lt_iff_le_not_ge, ← gci.l_le_l_iff, ← gi.u_le_u_iff, hf, hg]
    exact strictMono_inf_prod_sup hAB

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ Disjoint a (b ⊔ c)

Tactic:
disjoint_iff_inf_le,

Goal state after:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ a ⊓ (b ⊔ c) ≤ ⊥
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
h : x ≠ 0
⊢ ∃ x_1 y, x_1 ≠ y

Tactic:
use 0, ⟨x, Submodule.mem_span_singleton_self x⟩

Goal state after:
case h
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
h : x ≠ 0
⊢ 0 ≠ ⟨x, ⋯⟩
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
⊢ R ∙ x = ⊤ ↔ ∀ (v : M), ∃ r, r • x = v

Tactic:
by
  rw [eq_top_iff, le_span_singleton_iff]
  tauto

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case intro
ι : Sort u_1
α : Type u_3
inst✝² : ConditionallyCompleteLattice α
f : ι → α
s : Set α
inst✝¹ : Finite ι
inst✝ : Nonempty ι
hs : SupClosed s
hf : ∀ (i : ι), f i ∈ s
val✝ : Fintype (PLift ι)
⊢ (univ.sup' ⋯ fun i ↦ f i.down) ∈ s

Tactic:
exact hs.finsetSup'_mem Finset.univ_nonempty fun _ _ ↦ hf _

Goal state after:
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 ι'
hts : t ⊆ s
ht : image g t ⊆ image g s
i : ι'
his : i ∈ s
hi : g i ∈ image g s
hit : g i ∉ image g t
⊢ Disjoint (f (g i)) ((image g t).sup f)

Tactic:
sup_image

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 ι'
hts : t ⊆ s
ht : image g t ⊆ image g s
i : ι'
his : i ∈ s
hi : g i ∈ image g s
hit : g i ∉ image g t
⊢ Disjoint (f (g i)) (t.sup (f ∘ g))
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: 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 ∈ span R s, Commute y x

Tactic:
exact .span_left h

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
⊢ ∃ a, IsCoatom a ∧ x ≤ a

Tactic:
rcases exists_isCompl (xy.symm.IicOrderIsoIci ⟨a, ay⟩) with ⟨⟨b, xb⟩, hb⟩

Goal state after:
α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
b : α
xb : b ∈ Set.Ici x
hb : IsCompl (⋯.IicOrderIsoIci ⟨a, ay⟩) ⟨b, xb⟩
⊢ ∃ a, IsCoatom a ∧ x ≤ a
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i ↦ t.sup fun i' ↦ f (i, i')
ht : t.SupIndep fun i' ↦ s.sup fun i ↦ f (i, i')
⊢ (s ×ˢ t).SupIndep f

Tactic:
rw [Finset.product_eq_biUnion]
  apply Finset.SupIndep.biUnion
  · simpa using! hs
  · exact fun i' hi' ↦ (ht.mono fun i hi ↦ Finset.le_sup (f := fun i' ↦ f (i', i)) hi').image

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mpr
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i j : ι
hij : i ≠ j
huniv : ∀ (k : ι), k = i ∨ k = j
⊢ Disjoint (t i) (t j) → iSupIndep t

Tactic:
· rintro h k
    obtain rfl | rfl := huniv k
    · refine h.mono_right (iSup_le fun i => iSup_le fun hi => Eq.le ?_)
      rw [(huniv i).resolve_left hi]
    · refine h.symm.mono_right (iSup_le fun j => iSup_le fun hj => Eq.le ?_)
      rw [(huniv j).resolve_right hj]

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝¹ : CompleteLattice α
f : ι → α
inst✝ : IsCompactlyGenerated α
a : α
h : Directed (fun x1 x2 ↦ x1 ≤ x2) f
⊢ a ⊓ ⨆ i, f i = ⊥ ↔ ∀ (i : ι), a ⊓ f i = ⊥

Tactic:
h.inf_iSup_eq,

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝¹ : CompleteLattice α
f : ι → α
inst✝ : IsCompactlyGenerated α
a : α
h : Directed (fun x1 x2 ↦ x1 ≤ x2) f
⊢ ⨆ i, a ⊓ f i = ⊥ ↔ ∀ (i : ι), a ⊓ f i = ⊥
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: 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
x y : M
⊢ R ∙ x = R ∙ y ↔ ∃ z, z • x = y

Tactic:
by
  constructor
  · simp only [le_antisymm_iff, span_singleton_le_iff_mem, mem_span_singleton]
    rintro ⟨⟨a, rfl⟩, b, hb⟩
    rcases eq_or_ne y 0 with rfl | hy; · simp
    refine ⟨⟨b, a, ?_, ?_⟩, hb⟩
    · apply smul_left_injective R hy
      simpa only [mul_smul, one_smul]
    · rw [← hb] at hy
      apply smul_left_injective R (smul_ne_zero_iff.1 hy).2
      simp only [mul_smul, one_smul, hb]
  · rintro ⟨u, rfl⟩
    exact (span_singleton_group_smul_eq _ _ _).symm

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

Goal state before:
pp: case cons
R : Type u_5
inst✝ : NonUnitalNonAssocSemiring R
a x : R
xs : List R
ih : (∀ (b : R), b ∈ xs → Commute a b) → Commute a xs.sum
h : ∀ (b : R), b ∈ x :: xs → Commute a b
⊢ Commute a (x + xs.sum)

Tactic:
exact (h _ mem_cons_self).add_right (ih fun j hj ↦ h _ <| mem_cons_of_mem _ hj)

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
⊢ Disjoint b (⨆ t ∈ c, sSup t)

Tactic:
← sSup_image,

Goal state after:
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
⊢ Disjoint b (sSup (sSup '' c))
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
⊢ (fun x ↦ List.find? (fun b ↦ decide (p b)) l₁) ≍ fun x ↦ List.find? (fun b ↦ decide (p b)) l₂

Tactic:
refine Function.hfunext ?_ (fun hp₁ hp₂ _ ↦ heq_of_eq ?_)

Goal state after:
case refine_1
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
⊢ {x | x ∈ ⟦l₁⟧ ∧ p x}.Subsingleton = {x | x ∈ ⟦l₂⟧ ∧ p x}.Subsingleton

case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
hp₁ : {x | x ∈ ⟦l₁⟧ ∧ p x}.Subsingleton
hp₂ : {x | x ∈ ⟦l₂⟧ ∧ p x}.Subsingleton
x✝ : hp₁ ≍ hp₂
⊢ List.find? (fun b ↦ decide (p b)) l₁ = List.find? (fun b ↦ decide (p b)) l₂
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.pi fun x ↦ {True, False}, (fun a_1 x ↦ a_1 ∈ {a_2 ∈ s | ∃ (h : a_2 ∈ s), a a_2 h}) = a

Tactic:
by simp_rw [mem_filter, funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a x : α
b : M
⊢ (single a b) x ≠ 0 ↔ x = a ∧ b ≠ 0

Tactic:
simp [single_apply_eq_zero]

Goal state after: