mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ⇑F
sG : Surjective G
i : ι
h : ∀ (x : Quotient.out (g i)), ∃ x_1, G ⟨i, x_1⟩ i = x
⊢ g i ≤ f i

Tactic:
← mk_out (f i),

Goal state after:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ⇑F
sG : Surjective G
i : ι
h : ∀ (x : Quotient.out (g i)), ∃ x_1, G ⟨i, x_1⟩ i = x
⊢ g i ≤ #(Quotient.out (f i))
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g i))

Tactic:
← mk_out (f i),

Goal state after:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : #(Quotient.out (f i)) ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g i))
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
⊢ 1 < lift.{v, u} a ↔ 1 < a

Tactic:
by
  simpa using nat_lt_lift_iff (n := 1)

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

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
⊢ toENat #α = toENat #β

Tactic:
by
  rw [← toENat_lift, lift_mk_eq.{_, _, v}.mpr ⟨e⟩, toENat_lift]

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

Goal state before:
pp: α β : Type u
a : Cardinal.{u}
⊢ Small.{u, u + 1} ↑(Iic a)

Tactic:
← mk_out a

Goal state after:
α β : Type u
a : Cardinal.{u}
⊢ Small.{u, u + 1} ↑(Iic #(Quotient.out a))
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
h : IsSuccLimit c
⊢ ℵ₀ ≤ c

Tactic:
by
  contrapose! h
  exact not_isSuccLimit_of_lt_aleph0 h

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

Goal state before:
pp: α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ #↑t ≤ #↑{x | x ∈ s ∧ f x ∈ t}

Tactic:
convert! mk_preimage_of_subset_range _ _ h using 1

Goal state after:
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x ↦ f ↑x
⊢ #↑{x | x ∈ s ∧ f x ∈ t} = #↑((fun x ↦ f ↑x) ⁻¹' t)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
⊢ #α = 2 ↔ ∃ x y, x ≠ y ∧ {x, y} = univ

Tactic:
simp only [← @Nat.cast_two Cardinal, mk_eq_nat_iff_finset, Finset.card_eq_two]

Goal state after:
α : Type u
⊢ (∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}) ↔ ∃ x y, x ≠ y ∧ {x, y} = univ
Module: Mathlib.Algebra.Module.Hom

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst✝³ : Semiring S
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module S M
s s' : Sᵈᵐᵃ
f : M →+ M₂
m : M
⊢ ((s + s') • f) m = (s • f + s' • f) m

Tactic:
simp_rw [AddMonoidHom.add_apply, DomMulAct.smul_addMonoidHom_apply, ← map_add, ← add_smul]

Goal state after:
R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst✝³ : Semiring S
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module S M
s s' : Sᵈᵐᵃ
f : M →+ M₂
m : M
⊢ f (DomMulAct.mk.symm (s + s') • m) = f ((DomMulAct.mk.symm s + DomMulAct.mk.symm s') • m)
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_14
M : Type u_15
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c c✝ : R
x✝ : M
⊢ c • c✝ • x✝ = c✝ • c • x✝

Tactic:
simp only [smul_smul, mul_comm]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R M
x✝ : M₂
⊢ e.symm x✝ ∈ K ↔ x✝ ∈ comap (↑e.symm) K

Tactic:
mem_comap,

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
e : M ≃ₛₗ[τ₁₂] M₂
K : Submodule R M
x✝ : M₂
⊢ e.symm x✝ ∈ K ↔ ↑e.symm x✝ ∈ K
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
S : Type u_9
N : Type u_10
N₂ : Type u_11
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Semiring R
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module S N
inst✝ : Module S N₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule S N
qₗ : Submodule S N₂
f₁ f₂ : N →ₗ[S] N₂
h₁ : f₁ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}
h₂ : f₂ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}
⊢ pₗ ≤ comap f₁ qₗ ⊓ comap f₂ qₗ

Tactic:
rw [le_inf_iff]

Goal state after:
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
S : Type u_9
N : Type u_10
N₂ : Type u_11
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Semiring R
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N₂
inst✝¹ : Module S N
inst✝ : Module S N₂
τ₁₂ : R →+* R₂
p : Submodule R M
q : Submodule R₂ M₂
pₗ : Submodule S N
qₗ : Submodule S N₂
f₁ f₂ : N →ₗ[S] N₂
h₁ : f₁ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}
h₂ : f₂ ∈ {fₗ | pₗ ≤ comap fₗ qₗ}
⊢ pₗ ≤ comap f₁ qₗ ∧ pₗ ≤ comap f₂ qₗ
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: case mpr
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t → u ≤ s.prod t

Tactic:
· rintro ⟨hH, hK⟩ ⟨x1, x2⟩ h
    exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ M.nonUnitalSubsemiringClosure
⊢ x✝ ∈ NonUnitalSubsemiring.closure ↑M

Tactic:
rintro - ⟨H1, rfl⟩

Goal state after:
case refine_1
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ M.nonUnitalSubsemiringClosure
H1 : NonUnitalSubsemiring R
⊢ x✝ ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
⊢ s ∈ ↑M.nonUnitalSubsemiringClosure

Tactic:
rintro - ⟨H1, rfl⟩

Goal state after:
case refine_2
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
x✝ : R
hx : x✝ ∈ NonUnitalSubsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
⊢ s ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure
⊢ x✝ ∈ Subsemiring.closure ↑M

Tactic:
rintro - ⟨H1, rfl⟩

Goal state after:
case refine_1
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure
H1 : Subsemiring R
⊢ x✝ ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1
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✝ ∈ Subsemiring.closure ↑M
s : R
sM : s ∈ ↑M
⊢ s ∈ ↑M.subsemiringClosure

Tactic:
rintro - ⟨H1, rfl⟩

Goal state after:
case refine_2
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ Subsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
⊢ s ∈ (fun t ↦ ⋂ (_ : t ∈ {S | ↑M ⊆ ↑S}), ↑t) H1
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
x : M
n : ℕ
x✝ : n + 2 ≠ 1
h₁ : ¬IsUnit (x ^ (n + 2))
h₂ : ∀ ⦃a b : M⦄, x ^ (n + 2) = a * b → IsUnit a ∨ IsUnit b
this : IsUnit x ∨ IsUnit x
⊢ False

Tactic:
or_self

Goal state after:
M : Type u_2
inst✝ : Monoid M
x : M
n : ℕ
x✝ : n + 2 ≠ 1
h₁ : ¬IsUnit (x ^ (n + 2))
h₂ : ∀ ⦃a b : M⦄, x ^ (n + 2) = a * b → IsUnit a ∨ IsUnit b
this : IsUnit x
⊢ False
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p x y : M
h : Prime p
i : ℕ
hxy : p ^ (i + 1) ∣ x * y
⊢ ¬p ∣ y → p ^ (i + 1) ∣ x

Tactic:
exact fun a ↦ Prime.pow_dvd_of_dvd_mul_right h (i + 1) a hxy

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

Goal state before:
pp: case refine_1
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ ¬IsUnit (q ^ (m - n))

pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ q ^ m = q ^ n * q ^ (m - n)

Tactic:
· exact not_isUnit_of_not_isUnit_dvd hq (dvd_pow (dvd_refl _) (Nat.sub_pos_of_lt h).ne')

Goal state after:
case refine_2
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
q : M
hq : ¬IsUnit q
hq' : q ≠ 0
n m : ℕ
h : n < m
⊢ q ^ m = q ^ n * q ^ (m - n)
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
S : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : SetLike S M₀
inst✝ : SubmonoidClass S M₀
s : S
x : ↥s
hx : Irreducible x
h : ↑x = 0
⊢ IsUnit x

Tactic:
by simpa using hx.2 (a := x) (b := x) (by ext; simp [h])

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : a = b
⊢ a * ↑1 = b

Tactic:
rwa [Units.val_one, mul_one]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
⊢ nonZeroDivisorsRight M₀ = nonZeroDivisorsLeft M₀

Tactic:
nonZeroDivisorsLeft_eq_right

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
⊢ nonZeroDivisorsRight M₀ = nonZeroDivisorsRight M₀
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x : R
hx : x ∈ comap f (map f s)
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
mem_comap,

Goal state after:
case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x : R
hx : f x ∈ map f s
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case mpr
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
x✝ : ∃ x, x * a = 0 ∧ x ≠ 0
b : M₀
hb₁ : b * a = 0
hb₂ : b ≠ 0
⊢ Associates.mk b * Associates.mk a = 0

Tactic:
rw [Associates.mk_mul_mk, hb₁, Associates.mk_zero]

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 f g : A₁ ≃ₐ[R] A₂
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
obtain ⟨⟨f, _⟩, _⟩ := f

Goal state after:
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 g : A₁ ≃ₐ[R] A₂
f : A₁ → A₂
invFun✝ : A₂ → A₁
left_inv✝ : Function.LeftInverse invFun✝ f
right_inv✝ : Function.RightInverse invFun✝ f
map_mul'✝ :
  ∀ (x y : A₁),
    { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun (x * y) =
      { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun x *
        { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun y
map_add'✝ :
  ∀ (x y : A₁),
    { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun (x + y) =
      { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun x +
        { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun y
commutes'✝ :
  ∀ (r : R),
    { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun ((algebraMap R A₁) r) =
      (algebraMap R A₂) r
h₁ :
  { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_add' := map_add'✝, commutes' := commutes'✝ }.toFun =
    g.toFun
h₂ :
  { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
        map_add' := map_add'✝, commutes' := commutes'✝ }.invFun =
    g.invFun
⊢ { toFun := f, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝, map_mul' := map_mul'✝,
      map_add' := map_add'✝, commutes' := commutes'✝ } =
    g
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: case mp
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
⊢ f.ker ≤ p → ∃ y ∈ f.range, ⇑f ⁻¹' {y} ⊆ ↑p

pp: case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
⊢ (∃ y ∈ f.range, ⇑f ⁻¹' {y} ⊆ ↑p) → f.ker ≤ p

Tactic:
· intro h
    use 0
    rw [← SetLike.mem_coe, coe_range]
    exact ⟨⟨0, map_zero f⟩, h⟩

Goal state after:
case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
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₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
⊢ (∃ y ∈ f.range, ⇑f ⁻¹' {y} ⊆ ↑p) → f.ker ≤ p
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z : αᵒᵈ
xz : x✝ ≤ z
⊢ (x✝ ⊔ y) ⊓ z = x✝ ⊔ y ⊓ z

Tactic:
by
        rw [inf_comm, sup_comm, eq_comm, inf_comm, sup_comm]
        exact @sup_inf_assoc_of_le α _ _ _ y _ xz

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
s : Set M
p : (x : M) → x ∈ span R s → Prop
mem : ∀ (x : M) (h : x ∈ s), p x ⋯
zero : p 0 ⋯
add : ∀ (x y : M) (hx : x ∈ span R s) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯
smul : ∀ (a : R) (x : M) (hx : x ∈ span R s), p x hx → p (a • x) ⋯
x : M
hx : x ∈ span R s
⊢ p x hx

Tactic:
by
  let p : Submodule R M :=
    { carrier := { x | ∃ hx, p x hx }
      add_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, add _ _ _ _ hpx hpy⟩
      zero_mem' := ⟨_, zero⟩
      smul_mem' := fun r ↦ fun ⟨_, hpx⟩ ↦ ⟨_, smul r _ _ hpx⟩ }
  exact span_le (p := p) |>.mpr (fun y hy ↦ ⟨subset_span hy, mem y hy⟩) hx |>.elim fun _ ↦ id

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a x : α
h : IsAtom a
⊢ x < a ∨ x = a ↔ x = ⊥ ∨ x = a

Tactic:
h.lt_iff

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a x : α
h : IsAtom a
⊢ x = ⊥ ∨ x = a ↔ x = ⊥ ∨ x = a
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case empty
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
ht : ↑∅ ⊆ ↑(span R s)
⊢ ∃ T, ↑T ⊆ s ∧ ↑∅ ⊆ ↑(span R ↑T)

Tactic:
exact ⟨∅, by simp⟩

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : SupClosed s
⊢ SupClosed (infClosure s)

Tactic:
rintro _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
  rw [inf'_sup_inf']
  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
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b ↦ f ⟨i, b⟩
⊢ (s.sigma g).SupIndep f

Tactic:
rw [Finset.sigma_eq_biUnion]

Goal state after:
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b ↦ f ⟨i, b⟩
⊢ (s.biUnion fun i ↦ map (Function.Embedding.sigmaMk i) (g i)).SupIndep f
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case h.left
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := ⋯
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = d.sup id
⊢ ↑(c ∪ d) ⊆ s

Tactic:
simp only [hc.left, hd.left, Set.union_subset_iff, Finset.coe_union, and_self_iff]

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

Goal state before:
pp: case h
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
⊢ ∏ i ∈ s, f i = (∏ x, ⋯.choose) ^ 2

Tactic:
@sq,

Goal state after:
case h
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
⊢ ∏ i ∈ s, f i = (∏ x, ⋯.choose) * ∏ x, ⋯.choose
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → c ≤ sSup s → ∃ x ∈ s, c ≤ x
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
rw [le_inf_iff] at hcinf

Goal state after:
case pos
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → c ≤ sSup s → ∃ x ∈ s, c ≤ x
hcinf : c ≤ a ∧ c ≤ sSup s
⊢ c ≤ ⨆ b ∈ s, a ⊓ b
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mpr.add
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
x✝ x y : M
hx : x ∈ span R S
hy : y ∈ span R S
hx' : f ⟨x, hx⟩ = g ⟨x, hx⟩
hy' : f ⟨y, hy⟩ = g ⟨y, hy⟩
⊢ f ⟨x + y, ⋯⟩ = g ⟨x + y, ⋯⟩

Tactic:
f.map_add ⟨x, hx⟩ ⟨y, hy⟩,

Goal state after:
case mpr.add
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
x✝ x y : M
hx : x ∈ span R S
hy : y ∈ span R S
hx' : f ⟨x, hx⟩ = g ⟨x, hx⟩
hy' : f ⟨y, hy⟩ = g ⟨y, hy⟩
⊢ f ⟨x, hx⟩ + f ⟨y, hy⟩ = g ⟨x + y, ⋯⟩
Module: Mathlib.Order.CompactlyGenerated.Basic

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

Tactic:
rw [le_inf_iff] at hcinf

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
h : ∀ (s : Finset ι), s.SupIndep f
i✝ : ι
hf : InjOn f {i | f i ≠ ⊥}
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i✝}
t : Finset α := s.erase ⊥
i : ι
hi : i ∈ f ⁻¹' ↑t
j : ι
x✝ : j ∈ f ⁻¹' ↑t
hij : f i = f j
⊢ i = j

Tactic:
by
    refine hf ?_ ?_ hij <;> aesop (add norm simp [t])

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
hf : InjOn f {i | f i ≠ ⊥}
h : ∀ (s : Finset ι), s.SupIndep f
i✝ : ι
s : Finset α
hs : ↑s ⊆ f '' {j | j ≠ i✝}
t : Finset α := s.erase ⊥
i : ι
hi : i ∈ f ⁻¹' ↑t
j : ι
x✝ : j ∈ f ⁻¹' ↑t
hij : f i = f j
⊢ i = j

Tactic:
by
    refine hf ?_ ?_ hij <;> aesop (add norm simp [t])

Goal state after:
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: case intro
I : Type u_7
inst✝³ : DecidableEq I
M : I → Type u_8
inst✝² : (i : I) → CommMonoid (M i)
inst✝¹ : Finite I
N : Type u_9
inst✝ : CommMonoid N
g h : ((i : I) → M i) →* N
H : ∀ (i : I) (x : M i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)
val✝ : Fintype I
k : (i : I) → M i
⊢ ∏ x, g (Pi.mulSingle x (k x)) = ∏ x, h (Pi.mulSingle x (k x))

Tactic:
simp only [H]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Pi

Goal state before:
pp: ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : ((i : ι) → M i) →* M'
x✝ : (i : ι) → M i
⊢ ((fun φ ↦ ∏ i, (φ i).comp (evalMonoidHom M i)) ((fun φ i ↦ φ.comp (MonoidHom.mulSingle M i)) φ)) x✝ = φ x✝

Tactic:
simp only [MonoidHom.finsetProd_apply, MonoidHom.coe_comp, Function.comp_apply,
      evalMonoidHom_apply, MonoidHom.mulSingle_apply, ← map_prod]

Goal state after:
ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : ((i : ι) → M i) →* M'
x✝ : (i : ι) → M i
⊢ φ (∏ x, mulSingle x (x✝ x)) = φ x✝
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
⊢ iSupIndep fun k ↦ ⨅ i, f i (k i)

Tactic:
rw [iSupIndep_iff_supIndep]

Goal state after:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
⊢ ∀ (s : Finset ((i : ι) → κ i)), s.SupIndep fun k ↦ ⨅ i, f i (k i)