mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
v : ℕ
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Tactic:
rcases e : unpair v with ⟨v₁, v₂⟩
    have h := unpair_right_le v
    rw [e] at h
    rcases have : v₂ < succ v := lt_succ_of_le h
      denumerable_list_aux v₂ with
      ⟨a, h₁, h₂⟩
    rw [Option.mem_def] at h₁
    use ofNat α v₁ :: a
    simp [decodeList, e, h₂, h₁, encodeList, pair_eq_of_unpair_eq e]

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

Goal state before:
pp: n : ℕ
F : Type u → Type u
inst✝ : Applicative F
α β : Type u
f : α → F β
x : α
⊢ ∀ (xs : Vector α n), Vector.traverse f (x ::ᵥ xs) = cons <$> f x <*> Vector.traverse f xs

Tactic:
rintro ⟨xs, rfl⟩

Goal state after:
F : Type u → Type u
inst✝ : Applicative F
α β : Type u
f : α → F β
x : α
xs : List α
⊢ Vector.traverse f (x ::ᵥ ⟨xs, ⋯⟩) = cons <$> f x <*> Vector.traverse f ⟨xs, ⋯⟩
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f✝ : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : f✝.top = g.top
f : (Subrel (Sum.Lex r s) fun x ↦ Sum.Lex r s x f✝.top) ≃r r := f✝.subrelIso
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))

Tactic:
rw [h] at f

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f✝ : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : f✝.top = g.top
f : (Subrel (Sum.Lex r s) fun x ↦ Sum.Lex r s x g.top) ≃r r
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
o : Part α
⊢ map g (map f o) = map (g ∘ f) o

Tactic:
simp [map, Function.comp_assoc]

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ ⦃a : α⦄, (∀ (a_1 : ℕ), c a_1 ≤ a) → ωSup c ≤ a

Tactic:
exact fun ⦃a⦄ a_1 ↦ ωSup_le c a a_1

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
b : β
hb₀ : b ∈ f (c i)
hb₁ : y ∈ g (c i) b
⊢ y ∈ x

Tactic:
apply h''' b _

Goal state after:
case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
b : β
hb₀ : b ∈ f (c i)
hb₁ : y ∈ g (c i) b
⊢ y ∈ ωSup (c.map g) b

α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
b : β
hb₀ : b ∈ f (c i)
hb₁ : y ∈ g (c i) b
⊢ b ∈ ωSup (c.map f)
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)

Tactic:
have : Injective h := by
    refine (injective_piecewise_iff _).2 ⟨hf.injOn, ?_, ?_⟩
    · intro x hx y hy hxy
      obtain ⟨x', _, rfl⟩ : x ∈ g '' (f '' s)ᶜ := by rwa [hns]
      obtain ⟨y', _, rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
      rw [g'g _, g'g _] at hxy
      rw [hxy]
    · intro x hx y hy hxy
      obtain ⟨y', hy', rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
      rw [g'g _] at hxy
      exact hy' ⟨x, hx, hxy⟩

Goal state after:
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this✝ : Surjective h
this : Injective h
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
h✝ : succ (lift.{v, u} a) < lift.{v, u} (succ a)
b : Cardinal.{u}
h : b < succ a
hb : lift.{v, u} b = succ (lift.{v, u} a)
⊢ False

Tactic:
rw [lt_succ_iff, ← lift_le, hb] at h

Goal state after:
a : Cardinal.{u}
h✝ : succ (lift.{v, u} a) < lift.{v, u} (succ a)
b : Cardinal.{u}
h : succ (lift.{v, u} a) ≤ lift.{v, u} a
hb : lift.{v, u} b = succ (lift.{v, u} a)
⊢ False
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u}
h : c < ℵ₀
⊢ c = ↑(Classical.choose ⋯)

Tactic:
← Classical.choose_spec (lt_aleph0.1 h)

Goal state after:
c : Cardinal.{u}
h : c < ℵ₀
⊢ c = c
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: ⊢ StrictMonoOn (⇑toNat) (Iio ℵ₀)

Tactic:
simp only [← range_natCast, StrictMonoOn, forall_mem_range, toNat_natCast, Nat.cast_lt]

Goal state after:
⊢ ∀ (i i_1 : ℕ), i < i_1 → i < i_1
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_1.inl
h : sInf ∅ = 0
⊢ ∅ = ∅ ∨ ∃ a ∈ ∅, a = 0

pp: case refine_1.inr
s : Set Cardinal.{u_1}
h : sInf s = 0
hne : s.Nonempty
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0

Tactic:
· exact Or.inl rfl

Goal state after:
case refine_1.inr
s : Set Cardinal.{u_1}
h : sInf s = 0
hne : s.Nonempty
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹ : AddGroup M
inst✝ : DistribSMul R M
r : R
h : ∀ (m : M), r • m = 0 → m = 0
m₁ m₂ : M
eq : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ r • (m₁ - m₂) = 0

Tactic:
simp_rw [smul_sub, eq, sub_self]

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

Goal state before:
pp: a b : Cardinal.{u_1}
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b < ℵ₀ ↔ a < ℵ₀ ∧ b < ℵ₀

Tactic:
simp [mul_lt_aleph0_iff, ha, hb]

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

Goal state before:
pp: case pos
G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this : ∀ (x : G), x • 0 = 0
hb : b = 0
⊢ (g / h) • (a / b) = g • a / h • b

Tactic:
simp [hb, this]

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

Goal state before:
pp: case e_4.e_4
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
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ ⋯ ≍ snd✝

Tactic:
exact proof_irrel_heq ..

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

Goal state before:
pp: R : Type u_1
S : Type u_5
M₃ : Type u_11
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M₃
inst✝ : Module S M₃
σ : R →+* S
f g : R →ₛₗ[σ] M₃
h : f 1 = g 1
x : R
⊢ f x = g x

Tactic:
by rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h]

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_8
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₃
inst✝³ : Module R₁ M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →ₛₗ[σ₂₃] M₃
c : M
⊢ g 0 = 0

Tactic:
g.map_zero

Goal state after:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_8
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₃
inst✝³ : Module R₁ M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →ₛₗ[σ₂₃] M₃
c : M
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: case e_4.e_4
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 α
⊢ ⋯ ≍ snd✝

Tactic:
exact proof_irrel_heq ..

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

Goal state before:
pp: case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : FunLike F α β
inst✝ : SupSet α
x✝ : CompleteLattice β
⊢ ⊥ = sSup ((fun x ↦ ⊥) '' ∅)

Tactic:
rw [Set.image_empty, sSup_empty]

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₂
τ₂₁ : R₂ →+* R
inst✝ : RingHomInvPair τ₁₂ τ₂₁
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₁] M
h : g ∘ₛₗ f = id
m : M
hm : f m = 0
⊢ g 0 = 0

Tactic:
g.map_zero

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₂
τ₂₁ : R₂ →+* R
inst✝ : RingHomInvPair τ₁₂ τ₂₁
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₁] M
h : g ∘ₛₗ f = id
m : M
hm : f m = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_1
S : ι → NonUnitalSubsemiring R
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
by
  simp only [iInf, coe_sInf, Set.biInter_range]

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

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
S : ι → NonUnitalSubring R
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
by
  simp only [iInf, coe_sInf, Set.biInter_range]

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
S : ι → Subsemiring R
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
by
  simp only [iInf, coe_sInf, Set.biInter_range]

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

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

Tactic:
rw [algebraMap.smul', map_zero, smul_zero]

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

Goal state before:
pp: case mem.one
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : x ∈ closure s), p x 1 hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : R
hz : z ∈ s
⊢ p 1 z ⋯ ⋯

Tactic:
exact one_left _ _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : Add R
f : R ≃+* R
n : ℕ
⊢ ⇑(f ^ n) = (⇑f)^[n]

Tactic:
induction n with
  | zero =>
    simp
  | succ n ih =>
    ext
    simp [pow_succ, ih]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
⊢ ↑f.rangeS = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
by rw [coe_rangeS, coe_top]

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
ι : Sort u_1
S : ι → Subring R
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
by
  simp only [iInf, coe_sInf, Set.biInter_range]

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

Goal state before:
pp: case mem.one
R : Type u
inst✝ : NonAssocRing R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
one_left : ∀ (x : R) (hx : x ∈ closure s), p 1 x ⋯ hx
one_right : ∀ (x : R) (hx : x ∈ closure s), p x 1 hx ⋯
neg_left : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p (-x) y ⋯ hy
neg_right : ∀ (x y : R) (hx : x ∈ closure s) (hy : y ∈ closure s), p x y hx hy → p x (-y) hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y z : R
hz : z ∈ s
⊢ p 1 z ⋯ ⋯

Tactic:
exact one_left _ _

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

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

Tactic:
refine fun h => Or.imp (fun h' => ⟨?_, h'⟩) (fun h' => ⟨?_, h'⟩) (h.isUnit_or_isUnit rfl).symm

Goal state after:
case mp.refine_1
M : Type u_2
inst✝ : Monoid M
x y : M
h : Irreducible (x * y)
h' : IsUnit y
⊢ Irreducible x

case mp.refine_2
M : Type u_2
inst✝ : Monoid M
x y : M
h : Irreducible (x * y)
h' : IsUnit x
⊢ Irreducible y
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p q : M
h : DvdNotUnit p q
⊢ p ≠ q

Tactic:
by
  by_contra hcontra
  obtain ⟨hp, x, hx', hx''⟩ := h
  simp_all

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

Goal state before:
pp: case neg
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this✝ : a * (c * d) = a * 1
hcd : c * d = 1
this : a * c * (d * c) = a * c * 1
⊢ a ~ᵤ a * c

Tactic:
have hdc : d * c = 1 := mul_left_cancel₀ hac0 this

Goal state after:
case neg
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this✝ : a * (c * d) = a * 1
hcd : c * d = 1
this : a * c * (d * c) = a * c * 1
hdc : d * c = 1
⊢ a ~ᵤ a * c
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
h : Prime (x * y)
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Tactic:
rcases of_irreducible_mul h.irreducible with hx | hy

Goal state after:
case refine_1.inl
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
h : Prime (x * y)
hx : IsUnit x
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

case refine_1.inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
x y : M
h : Prime (x * y)
hy : IsUnit y
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₂
h : p₁ ^ k₁ = p₂ ^ k₂
⊢ p₁ = p₂

Tactic:
by
  rw [← associated_iff_eq] at h ⊢
  apply h.of_pow_associated_of_prime' hp₁ hp₂ hk₁

Goal state after:
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₂
p : Submodule R₂ M₂
⊢ f.range ≤ p ↔ comap f p = ⊤

Tactic:
range_eq_map,

Goal state after:
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₂
p : Submodule R₂ M₂
⊢ map f ⊤ ≤ p ↔ comap f p = ⊤
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
⊢ q ∣ p ^ (n + 1) ↔ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
refine ⟨fun h => ?_, fun ⟨i, hi, hq⟩ => hq.dvd.trans (pow_dvd_pow p hi)⟩

Goal state after:
case succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p ^ (n + 1)
⊢ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case mp.add
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
N : Submodule R M
inst✝ : SMulCommClass R S M
r : S
x m₁ : M
h₁ : m₁ ∈ N
mem₁ : r • m₁ ∈ {r} • N
m₂ : M
h₂ : m₂ ∈ N
mem₂ : r • m₂ ∈ {r} • N
⊢ ∃ m ∈ N, r • m₁ + r • m₂ = r • m

Tactic:
exact ⟨m₁ + m₂, Submodule.add_mem _ h₁ h₂, by simp⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
h : IsAtomic α
b : αᵒᵈ
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

Tactic:
apply h.eq_bot_or_exists_atom_le

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : IsAtomic αᵒᵈ
b : α
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

Tactic:
apply h.eq_bot_or_exists_atom_le

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 y z : M
⊢ z ∈ span R {x, y} ↔ ∃ a b, a • x + b • y = z

Tactic:
mem_span_insert,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
⊢ (∃ a, ∃ z_1 ∈ R ∙ y, z = a • x + z_1) ↔ ∃ a b, a • x + b • y = z
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : SupClosed s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ ((t ×ˢ u).inf' ⋯ fun i ↦ id i.1 ⊔ id i.2) ∈ infClosure s

Tactic:
exact finsetInf'_mem_infClosure _
    fun i hi ↦ hs (hts (mem_product.1 hi).1) (hus (mem_product.1 hi).2)

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 ι
⊢ t ⊆ image g s → ∀ ⦃i : ι⦄, i ∈ image g s → i ∉ t → Disjoint (f i) (t.sup f)

Tactic:
ht

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 ι
ht : t ⊆ image g s
⊢ ∀ ⦃i : ι⦄, i ∈ image g s → i ∉ t → Disjoint (f i) (t.sup f)
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ∀ x ≤ b, ¬a ⋖ x
⊢ x ≤ a

Tactic:
specialize hcon (x ⊔ a) (sup_le (hsb.1 hx) hab.le)

Goal state after:
α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
⊢ x ≤ a
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_2
ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomistic (π i)
s : (i : ι) → π i
i : ι
⊢ s i ∈ lowerBounds (upperBounds (Function.eval i '' {f | (∃ i a, IsAtom a ∧ f = Function.update ⊥ i a) ∧ f ≤ s}))

Tactic:
refine fun j hj ↦ (isLUB_atoms_le (s i)).2 fun x ⟨hx₁, hx₂⟩ ↦ ?_
      exact hj ⟨Function.update ⊥ i x, ⟨⟨_, x, hx₁, rfl⟩, by simp [update_le_iff, hx₂]⟩, by simp⟩

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
s : Finset ι
f : ι → α
⊢ iSupIndep (f ∘ Subtype.val) ↔ s.SupIndep f

Tactic:
by
  classical
    rw [Finset.supIndep_iff_disjoint_erase]
    refine Subtype.forall.trans (forall₂_congr fun a b => ?_)
    rw [Finset.sup_eq_iSup]
    congr! 1
    refine iSup_subtype.trans ?_
    congr! 1
    simp [iSup_and, @iSup_comm _ (_ ∈ s)]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Tactic:
refine ⟨t, ht₁, (sSup_le fun y hy => ?_).antisymm ?_⟩

Goal state after:
case refine_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
y : α
hy : y ∈ s
⊢ y ≤ t.sup id

case refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
⊢ t.sup id ≤ sSup s
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
s t : Set ι
hf : iSupIndep f
hst : Disjoint s t
hs : s.Finite
⊢ Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)

Tactic:
by
  suffices ∀ (s : Finset ι) (hst : Disjoint ↑s t), Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i) by
    specialize this hs.toFinset
    aesop
  clear! s
  intro s hst
  classical
  induction s using Finset.induction_on generalizing t with
  | empty => simp
  | insert j s₀ hj ih =>
    have hjt : j ∉ t := by aesop
    replace hst : Disjoint ↑s₀ (insert j t) := by aesop
    replace ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i) := by
      specialize ih hst
      rwa [iSup_insert] at ih
    have : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ (⨆ i ∈ (s₀ : Set ι), f i)) := by
      rw [← iSup_union]
      exact disjoint_biSup hf <| by aesop
    rw [s₀.iSup_insert j f, disjoint_comm, sup_comm]
    exact disjoint_sup_right_of_disjoint_sup_right ih this

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:
rw [← hb] at hy

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