mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ₗ β
⊢ a ≤ b ∧ ¬b ≤ a → a < b

Tactic:
· rintro ⟨⟨hab⟩ | ⟨hab⟩ | ⟨a, b⟩, hba⟩
        · exact Lex.inl (hab.lt_of_not_ge fun h => hba <| Lex.inl h)
        · exact Lex.inr (hab.lt_of_not_ge fun h => hba <| Lex.inr h)
        · exact Lex.sep _ _

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

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s : Set α
a : α
hs : IsUpperSet s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ ∀ b ∈ s, ∀ c ∈ {a}, b ≤ c → b ∈ {a}

Tactic:
simpa using has

Goal state after:
Module: Mathlib.Order.InitialSeg

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

Tactic:
by
  intro b h
  simpa using mem_range_of_rel_top _ h

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

Goal state before:
pp: case mpr
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
⊢ (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂

Tactic:
calc
      f^[n₁ + n₂] (a₁ ⊔ a₂) = f^[n₁] (f^[n₂] (a₁ ⊔ a₂)) :=
        Function.iterate_add_apply f n₁ n₂ _
      _ = f^[n₁] (f^[n₂] (a₂ ⊔ a₁)) := by rw [sup_comm]
      _ ≤ f^[n₁] (f^[n₂] a₂ ⊔ a₁) := f.mono.iterate n₁ (h' n₂ _ _)
      _ = f^[n₁] (a₁ ⊔ f^[n₂] a₂) := by rw [sup_comm]
      _ ≤ f^[n₁] a₁ ⊔ f^[n₂] a₂ := h' n₁ a₁ _

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case inr
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x

Tactic:
rw [Part.eq_some_iff] at h₀

Goal state after:
case inr
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x
Module: Mathlib.Order.BourbakiWitt

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

Tactic:
exact le_trans hyz (le_map z)

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self
α : 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
⊢ z < f y → f z ≤ f y

Tactic:
hzy

Goal state after:
case image_self_subset_self
α : 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
⊢ f z ≤ f y
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case mk
α β : Type u_1
h : #α < #β
f : α ↪ β
hf : ¬Surjective ⇑f
⊢ #α + 1 ≤ #β

Tactic:
rw [Surjective, not_forall] at hf

Goal state after:
case mk
α β : Type u_1
h : #α < #β
f : α ↪ β
hf : ∃ x, ¬∃ a, f a = x
⊢ #α + 1 ≤ #β
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h : ¬∃ i, Surjective fun x ↦ ↑x i
⊢ ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y

Tactic:
simpa [Surjective] using h

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

Goal state before:
pp: case inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x = f
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

Tactic:
rcases hy with hy | hy

Goal state after:
case inl.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x = f
hy : y = f
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x = f
hy : y ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hy : y ∈ insert f s
hx : x ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

Tactic:
rcases hy with hy | hy

Goal state after:
case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y = f
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

case inr.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
hn : n ≠ 0
⊢ (toENat c).toNat = n ↔ c = ↑n

Tactic:
ENat.toNat_eq_iff hn,

Goal state after:
c : Cardinal.{u}
n : ℕ
hn : n ≠ 0
⊢ toENat c = ↑n ↔ c = ↑n
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: case inr
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ¬ℵ₀ ≤ c
hd : ¬ℵ₀ ≤ d
⊢ toNat c = toNat d

Tactic:
· apply eq_of_forall_le_iff
    rw [← cast_toNat_of_lt_aleph0 (not_le.mp hc), ← cast_toNat_of_lt_aleph0 (not_le.mp hd)] at h
    simpa using h

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

Goal state before:
pp: n : ℕ
hx : ↑n < ℵ₀
⊢ 2 ^ ↑n < ℵ₀

Tactic:
exact mod_cast natCast_lt_aleph0

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

Goal state before:
pp: a b : Cardinal.{u}
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0
⊢ b ≠ 0 ∧ ℵ₀ ≤ a ∨ a ≠ 0 ∧ ℵ₀ ≤ b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0

Tactic:
simp only [and_comm, or_comm]

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

Goal state before:
pp: α : Type u
S T : Set α
h : T ⊆ S
⊢ #↑(S \ T) + #↑T = #↑S

Tactic:
by
  refine (mk_union_of_disjoint <| ?_).symm.trans <| by rw [sdiff_union_of_subset h]
  exact disjoint_sdiff_self_left

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst✝⁸ : Semiring R₁
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring R₃
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
σ₃₂ : R₃ →+* R₂
inst✝¹ : RingHomInvPair σ₂₃ σ₃₂
inst✝ : RingHomCompTriple σ₁₃ σ₃₂ σ₁₂
hf : ∃ f', f ∘ₛₗ f' = id
⊢ Surjective fun g ↦ f ∘ₛₗ g

Tactic:
intro h
  obtain ⟨f', hf'⟩ := hf
  refine ⟨f'.comp h, ?_⟩
  simp_rw [← comp_assoc, hf', id_comp]

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : i ∉ s
ih : ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
⊢ ↑(p i ⊓ s.inf p) = ⋂ i_1 ∈ insert i s, ↑(p i_1)

Tactic:
coe_inf,

Goal state after:
case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : i ∉ s
ih : ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
⊢ ↑(p i) ∩ ↑(s.inf p) = ⋂ i_1 ∈ insert i s, ↑(p i_1)
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
s : Set (Submodule R M)
t : R
m : M
h : m ∈ (sSup (toAddSubmonoid '' s)).carrier
⊢ t • m ∈ (sSup (toAddSubmonoid '' s)).carrier

Tactic:
by
        simp_rw [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, sSup_eq_iSup'] at h ⊢
        induction h using AddSubmonoid.iSup_induction' with
        | mem p x hx =>
          obtain ⟨-, ⟨p : Submodule R M, hp : p ∈ s, rfl⟩⟩ := p
          suffices p.toAddSubmonoid ≤ ⨆ q : toAddSubmonoid '' s, (q : AddSubmonoid M) by
            exact this (smul_mem p t hx)
          apply le_sSup
          rw [Subtype.range_coe_subtype]
          exact ⟨p, hp, rfl⟩
        | zero => simpa only [smul_zero] using zero_mem _
        | add _ _ _ _ mx my => revert mx my; simp_rw [smul_add]; exact add_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✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
s : Set (Submodule R M)
hs : sSup s = ⊤
h : ∀ m ∈ s, f ∘ₛₗ m.subtype = 0
⊢ f.ker = ⊤

Tactic:
eq_top_iff,

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₂
f : M →ₛₗ[τ₁₂] M₂
s : Set (Submodule R M)
hs : sSup s = ⊤
h : ∀ m ∈ s, f ∘ₛₗ m.subtype = 0
⊢ ⊤ ≤ f.ker
Module: Mathlib.Algebra.Ring.CharZero

Goal state before:
pp: α : Type u_1
R : Type u_2
S : Type u_3
n : ℕ
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
⊢ 2 ≠ 0

Tactic:
decide

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

Goal state before:
pp: case mp
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₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ (∃ y ∈ p, ↑e y = x) → e.symm x ∈ p

Tactic:
rintro ⟨y, hy, hx⟩

Goal state after:
case mp
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₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
y : M
hy : y ∈ p
hx : ↑e y = x
⊢ e.symm x ∈ p
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_4
inst✝¹ : Semiring S
inst✝ : Algebra R S
⊢ algebraMapSubmonoid S (IsUnit.submonoid R) ≤ IsUnit.submonoid S

Tactic:
rintro x ⟨y, hy, rfl⟩

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_4
inst✝¹ : Semiring S
inst✝ : Algebra R S
y : R
hy : y ∈ ↑(IsUnit.submonoid R)
⊢ (algebraMap R S) y ∈ IsUnit.submonoid S
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ f ((algebraMap R A) r * a) = (algebraMap R B) r * f a

Tactic:
rw [← Algebra.smul_def, ← Algebra.smul_def, map_smul]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
h : x ∈ closure s
⊢ x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
by
    induction h using closure_induction with
    | mem _ hx => exact AddSubgroup.subset_closure (Subsemigroup.subset_closure hx)
    | zero => exact zero_mem _
    | add _ _ _ _ hx hy => exact add_mem hx hy
    | neg x _ hx => exact neg_mem hx
    | mul _ _ _hx _hy hx hy =>
      clear _hx _hy
      induction hx, hy using AddSubgroup.closure_induction₂ with
      | mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
      | zero_left => simp
      | zero_right => simp
      | add_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
      | add_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
      | neg_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
      | neg_right _ _ _ _ h => simpa [mul_neg] using neg_mem h

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
S : Set (NonUnitalSubring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
have : Nonempty S := Sne.to_subtype
  simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists,
    exists_prop]

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
f : A →+* B
h : ∀ (c : R) (x : A), f (c • x) = c • f x
c : R
⊢ f ((algebraMap R A) c) = (algebraMap R B) c

Tactic:
by simp only [Algebra.algebraMap_eq_smul_one, h, f.map_one]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝ : R
hx✝ : x✝ ∈ closure s
hx : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ -x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
| neg _ _ hx =>

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Set R
x : R
hx : x ∈ closure s
⊢ f x ∈ closure (⇑f '' s)

Tactic:
rw [← f.map_closure, Subring.mem_map]
  exact ⟨x, hx, rfl⟩

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

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

Tactic:
← HAB,

Goal state after:
case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : ↑u * y = A * B
⊢ y = ↑u⁻¹ * (↑u * y)
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

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

Tactic:
← HAB,

Goal state after:
case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y * ↑u = A * B
⊢ y = y * ↑u * ↑u⁻¹
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
y : M
ha : Irreducible (y ^ 2)
⊢ 2 ≠ 1

Tactic:
decide

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

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

Tactic:
apply dvd_pow_self _ hk₁.ne'

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ Irreducible (Associates.mk a) ↔ Irreducible a

Tactic:
simp only [irreducible_iff, isUnit_mk, forall_associated, isUnit_mk, mk_mul_mk,
    mk_eq_mk_iff_associated, Associated.comm (x := a)]

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ (¬IsUnit a ∧ ∀ (a_1 a_2 : M), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) ↔
    ¬IsUnit a ∧ ∀ ⦃a_1 b : M⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
a : M
⊢ (∀ ⦃a_1 b : M⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b) → ∀ (a_2 a_3 : M), a_2 * a_3 ~ᵤ a → IsUnit a_2 ∨ IsUnit a_3

Tactic:
rintro h x y ⟨u, rfl⟩

Goal state after:
case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
x y : M
u : Mˣ
h : ∀ ⦃a b : M⦄, x * y * ↑u = a * b → IsUnit a ∨ IsUnit b
⊢ IsUnit x ∨ IsUnit y
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
q : Submodule R₂ M₂
⊢ f.range ⊓ q ≤ map f (comap f q)

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

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

Goal state before:
pp: case pos
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
h : 0 ∈ s
⊢ span R (s \ {0}) = span R s

Tactic:
← span_insert_zero,

Goal state after:
case pos
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
h : 0 ∈ s
⊢ span R (insert 0 (s \ {0})) = span R s
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : IsModularLattice α
a b : α
inst✝¹ : BoundedOrder α
inst✝ : ComplementedLattice α
h : a ≤ b
⊢ ∃ a', a ⊓ a' = ⊥ ∧ a ⊔ a' = b

Tactic:
apply exists_inf_eq_and_sup_eq (by simp) h

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
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = x

Tactic:
refine span_induction ?_ ?_ ?_ ?_ h

Goal state after:
case refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
⊢ ∀ x ∈ ↑p ∪ ↑p', ∃ y ∈ p, ∃ z ∈ p', y + z = x

case refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
⊢ ∃ y ∈ p, ∃ z ∈ p', y + z = 0

case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
⊢ ∀ (x y : M),
    x ∈ span R (↑p ∪ ↑p') →
      y ∈ span R (↑p ∪ ↑p') →
        (∃ y ∈ p, ∃ z ∈ p', y + z = x) → (∃ y_1 ∈ p, ∃ z ∈ p', y_1 + z = y) → ∃ y_1 ∈ p, ∃ z ∈ p', y_1 + z = x + y

case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
⊢ ∀ (a : R), ∀ x ∈ span R (↑p ∪ ↑p'), (∃ y ∈ p, ∃ z ∈ p', y + z = x) → ∃ y ∈ p, ∃ z ∈ p', y + z = a • x
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u.sup' hu id, v.sup' hv id) ∈ supClosure (s ×ˢ t)

Tactic:
refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ ↑(u ×ˢ v) ⊆ s ×ˢ t

case refine_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u ×ˢ v).sup' ⋯ id = (u.sup' hu id, v.sup' hv id)
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 y : M
h : x ∈ R ∙ y
⊢ ∃ a, a • y = x

Tactic:
refine span_induction ?_ ?_ ?_ ?_ h

Goal state after:
case refine_1
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
⊢ ∀ x ∈ {y}, ∃ a, a • y = x

case refine_2
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, a • y = 0

case refine_3
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
⊢ ∀ (x y_1 : M), x ∈ R ∙ y → y_1 ∈ R ∙ y → (∃ a, a • y = x) → (∃ a, a • y = y_1) → ∃ a, a • y = x + y_1

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
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:
eq_top_iff,

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

Goal state before:
pp: case left
α : 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
⊢ latticeClosure s ⊆ f ⁻¹' latticeClosure (f '' s)

Tactic:
apply latticeClosure_sup_inf_induction

Goal state after:
case left.mem
α : 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
⊢ ∀ a ∈ s, a ∈ f ⁻¹' latticeClosure (f '' s)

case sup
α : 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
⊢ ∀ a ∈ latticeClosure s,
    ∀ b ∈ latticeClosure s,
      a ∈ f ⁻¹' latticeClosure (f '' s) → b ∈ f ⁻¹' latticeClosure (f '' s) → a ⊔ b ∈ f ⁻¹' latticeClosure (f '' s)

case left.inf
α : 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
⊢ ∀ a ∈ latticeClosure s,
    ∀ b ∈ latticeClosure s,
      a ∈ f ⁻¹' latticeClosure (f '' s) → b ∈ f ⁻¹' latticeClosure (f '' s) → a ⊓ b ∈ f ⁻¹' latticeClosure (f '' s)
Module: Mathlib.Order.SupClosed

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

Tactic:
apply latticeClosure_sup_inf_induction

Goal state after:
case right.mem
α : 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
⊢ ∀ a ∈ f '' s, a ∈ f '' latticeClosure s

case sup
α : 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
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊔ b ∈ f '' latticeClosure s

case right.inf
α : 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
⊢ ∀ a ∈ latticeClosure (f '' s),
    ∀ b ∈ latticeClosure (f '' s), a ∈ f '' latticeClosure s → b ∈ f '' latticeClosure s → a ⊓ b ∈ f '' latticeClosure s