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

Goal state before:
pp: case refine_2
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin (s.length + 1) ↪ Fin (t.length + 1)
hit : t.toFun ∘ ⇑i = s.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last s.length) = Fin.last t.length
⊢ t.toFun (i (Fin.last s.length)) = s.toFun (Fin.last s.length)

Tactic:
← hit,

Goal state after:
case refine_2
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin (s.length + 1) ↪ Fin (t.length + 1)
hit : t.toFun ∘ ⇑i = s.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last s.length) = Fin.last t.length
⊢ t.toFun (i (Fin.last s.length)) = (t.toFun ∘ ⇑i) (Fin.last s.length)
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ -(x + y) + (x + y) = 0

Tactic:
rw [← this]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
this : -x + x + (-y + y) = 0
⊢ -(x + y) + (x + y) = -x + x + (-y + y)
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case insert.mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
x : α
y : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ ∀ {i_1 : ι}, i_1 ∈ insert i is → update g i x i_1 ∈ f i_1

Tactic:
intro j hj
        obtain rfl | hj := Finset.mem_insert.mp hj
        · rwa [Function.update_self]
        · rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]
          exact hg hj

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Submonoid R
⊢ S ≤ nonZeroDivisorsLeft R ↔ ∀ (s : ↥S), IsLeftRegular ↑s

Tactic:
SetLike.le_def,

Goal state after:
R : Type u_1
inst✝ : Ring R
S : Submonoid R
⊢ (∀ ⦃x : R⦄, x ∈ S → x ∈ nonZeroDivisorsLeft R) ↔ ∀ (s : ↥S), IsLeftRegular ↑s
Module: Mathlib.Algebra.Ring.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Submonoid R
⊢ S ≤ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRightRegular ↑s

Tactic:
SetLike.le_def,

Goal state after:
R : Type u_1
inst✝ : Ring R
S : Submonoid R
⊢ (∀ ⦃x : R⦄, x ∈ S → x ∈ nonZeroDivisorsRight R) ↔ ∀ (s : ↥S), IsRightRegular ↑s
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Fintype ι
S : ι → Set α
⊢ (fun f ↦ ∏ i, f i) '' univ.pi S = ∏ i, S i

Tactic:
by
  simpa only [Finset.coe_univ] using image_finsetProd_pi Finset.univ S

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ a b c : α
hbc : (fun x1 x2 ↦ x1 ≤ x2) b c
⊢ a * (c + b) = (fun x1 x2 ↦ x1 * x2) a c

Tactic:
hbc.add_eq_left

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ a b c : α
hbc : (fun x1 x2 ↦ x1 ≤ x2) b c
⊢ a * c = (fun x1 x2 ↦ x1 * x2) a c
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ a b c : α
hbc : (fun x1 x2 ↦ x1 ≤ x2) b c
⊢ (c + b) * a = swap (fun x1 x2 ↦ x1 * x2) a c

Tactic:
hbc.add_eq_left

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ a b c : α
hbc : (fun x1 x2 ↦ x1 ≤ x2) b c
⊢ c * a = swap (fun x1 x2 ↦ x1 * x2) a c
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case succ
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
⊢ ∀ (hx : x ∈ M ^ n * M), C (n + 1) x ⋯

Tactic:
exact fun hx ↦ Submodule.mul_induction_on' (fun m hm x ih => mul_mem _ _ hm (n_ih _) _ ih)
      (fun x hx y hy Cx Cy => add _ _ _ _ _ Cx Cy) hx

Goal state after:
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : R
⊢ (∃ x_1 ∈ I.prod J, (RingHom.fst R S) x_1 = x) → x ∈ I

Tactic:
by
      rintro ⟨x, ⟨h, rfl⟩⟩
      exact h.1

Goal state after:
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: case mp.inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
hI : ((map (RingHom.fst R S) I).prod ⊤).IsPrime
h : map (RingHom.snd R S) I = ⊤
⊢ ∃ p, p.IsPrime ∧ (map (RingHom.fst R S) I).prod ⊤ = p.prod ⊤

Tactic:
exact ⟨_, ⟨isPrime_of_isPrime_prod_top hI, rfl⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
r : R i
⊢ r ∈ map (Pi.evalRingHom R i) (pi I) ↔ r ∈ I i

Tactic:
mem_map_iff_of_surjective (Pi.evalRingHom R i) (Function.surjective_eval _)

Goal state after:
ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
r : R i
⊢ (∃ x ∈ pi I, (Pi.evalRingHom R i) x = r) ↔ r ∈ I i
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m✝ : M
hm✝ : m✝ ∈ span R T
m : M
hm : m ∈ T
r : R
hr : r ∈ Ideal.span S
⊢ 0 • m ∈ span R (S • T)

Tactic:
by rw [zero_smul]; exact zero_mem _

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : gcd x y = 0
⊢ x * y / gcd x y ∣ z

Tactic:
rw [hxy, div_zero]
    rw [EuclideanDomain.gcd_eq_zero_iff] at hxy
    rwa [hxy.1] at hxz

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
h : n ≠ 0
⊢ I ^ (m + n) = I ^ m * I ^ n

Tactic:
exact Submodule.pow_add _ h

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
h : 1 ∈ I ⊔ J
i : R
hi : i ∈ I ⊔ K
⊢ i ∈ I ⊔ J * K

Tactic:
rw [Submodule.mem_sup] at h hi ⊢

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
h : ∃ y ∈ I, ∃ z ∈ J, y + z = 1
i : R
hi : ∃ y ∈ I, ∃ z ∈ K, y + z = i
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
I : Ideal R
⊢ I ≤ N.annihilator ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ ⊥

Tactic:
SetLike.le_def,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
I : Ideal R
⊢ (∀ ⦃x : R⦄, x ∈ I → x ∈ N.annihilator) ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
h : 1 ∈ I ⊔ K
i : R
hi : i ∈ I ⊔ J
⊢ i ∈ I ⊔ J * K

Tactic:
rw [Submodule.mem_sup] at h hi ⊢

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
h : ∃ y ∈ I, ∃ z ∈ K, y + z = 1
i : R
hi : ∃ y ∈ I, ∃ z ∈ J, y + z = i
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
e : R ≃+* S
⊢ ∀ {a b : Ideal S},
    { toFun := fun I ↦ Ideal.comap e I, invFun := fun I ↦ Ideal.map e I, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun I ↦ Ideal.comap e I, invFun := fun I ↦ Ideal.map e I, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
simp [← Ideal.map_le_iff_le_comap, Ideal.map_comap_of_surjective _ e.surjective]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ I.radical = I ↔ I.IsRadical

Tactic:
by
  rw [le_antisymm_iff, and_iff_left le_radical, IsRadical]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
r : R
hr : r ∈ sInf {J | I ≤ J ∧ J.IsPrime}
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun x ↦ x ∈ {K | r ∉ K.radical}) m
hrm : r ∉ m.radical
x : R
hxm : x ∉ m
hrmx : r ∉ (m ⊔ span {x}).radical
⊢ x ∈ m

Tactic:
by
          rw [hm.eq_of_le hrmx le_sup_left]
          exact Submodule.mem_sup_right <| mem_span_singleton_self x

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J P : Ideal R
hp : P.IsPrime
⊢ (∀ r ∈ I, ∀ s ∈ J, r ∈ P ∨ s ∈ P) ↔ J ≤ P ∨ I ≤ P

Tactic:
SetLike.le_def,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I J P : Ideal R
hp : P.IsPrime
⊢ (∀ r ∈ I, ∀ s ∈ J, r ∈ P ∨ s ∈ P) ↔ (∀ ⦃x : R⦄, x ∈ J → x ∈ P) ∨ ∀ ⦃x : R⦄, x ∈ I → x ∈ P
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
⊢ generator S ∈ S

Tactic:
by
  have : generator S ∈ span R {generator S} := subset_span (mem_singleton _)
  convert! this
  exact span_singleton_generator S |>.symm

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b c : α
ac : a ∣ c
ab : a ∣ b
⊢ a ∣ if c = 0 then b else if b = 0 then c else Classical.choose ⋯

Tactic:
split_ifs with h h_1
      · exact ab
      · exact ac
      have h0 : lcm c b ≠ 0 := by
        intro con
        have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left c rfl)
        rw [con, zero_dvd_iff, mul_eq_zero] at h
        cases h
        · exact absurd ‹c = 0› h
        · exact absurd ‹b = 0› h_1
      rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd c b)]
      rcases ab with ⟨d, rfl⟩
      rw [mul_eq_zero] at ‹a * d ≠ 0›
      push Not at h_1
      rw [mul_comm a, ← mul_assoc, mul_dvd_mul_iff_right h_1.1]
      apply lcm_dvd (Dvd.intro d rfl)
      rw [mul_comm, mul_dvd_mul_iff_right h_1.2]
      apply ac

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝ : AddMonoid α
A : Matrix m n α
⊢ (∃ b, A + b = 0 ∧ b + A = 0) ↔ ∀ (i : m) (j : n), ∃ b, A i j + b = 0 ∧ b + A i j = 0

Tactic:
Classical.skolem,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝ : AddMonoid α
A : Matrix m n α
⊢ (∃ b, A + b = 0 ∧ b + A = 0) ↔ ∃ f, ∀ (x : m) (x_1 : n), A x x_1 + f x x_1 = 0 ∧ f x x_1 + A x x_1 = 0
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: l : Type u_1
m : Type u_2
n✝ : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n✝
inst✝ : AddGroupWithOne α
n : ℕ
⊢ (diagonal fun x ↦ ↑↑n) = diagonal fun x ↦ ↑n

Tactic:
rw [Int.cast_natCast]

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case intro.intro
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ P M

Tactic:
matrix_eq_sum_single M,

Goal state after:
case intro.intro
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ P (∑ i, ∑ j, single i j (M i j))
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift.{?u.31, v} #β
⊢ lift.{u, v} #β ^ Fintype.card α = max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
rw [max_eq_right (le_trans _ this), power_nat_eq this]

Goal state after:
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift.{u, v} #β
⊢ 1 ≤ Fintype.card α

α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
this : ℵ₀ ≤ lift.{u, v} #β
⊢ lift.{v, u} #α ≤ ℵ₀
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
c : ↑T
ci : (i : ι) → ↑(S i)
hci : ∀ (i : ι), ↑(ci i) = ↑c
cβ : β
h : ∀ (i : ι), f i (ci i) = cβ
⊢ iUnionLift S f hf T hT c = cβ

Tactic:
let ⟨i, hi⟩ := Set.mem_iUnion.1 (hT c.prop)

Goal state after:
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
c : ↑T
ci : (i : ι) → ↑(S i)
hci : ∀ (i : ι), ↑(ci i) = ↑c
cβ : β
h : ∀ (i : ι), f i (ci i) = cβ
i : ι
hi : ↑c ∈ S i
⊢ iUnionLift S f hf T hT c = cβ
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : (toMultiset f).toFinset = f.support
⊢ Disjoint {a} f.support

Tactic:
Finset.disjoint_singleton_left

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : a ∉ f.support
hn : n ≠ 0
ih : (toMultiset f).toFinset = f.support
⊢ a ∉ f.support
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
f : α →₀ ℕ
i : α
⊢ f i ≠ 0 ↔ i ∈ f.support

Tactic:
Finsupp.mem_support_iff

Goal state after:
α : Type u_1
f : α →₀ ℕ
i : α
⊢ f i ≠ 0 ↔ f i ≠ 0
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) * lift.{v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{v, w} (Module.rank F A)

Tactic:
← lift_umax.{w, v},

Goal state after:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{max w v, w} (Module.rank F A)
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: case pos
R : Type u
inst✝¹¹ : Semiring R
inst✝¹⁰ : StrongRankCondition R
S : Type u_2
T : Type u_3
inst✝⁹ : Semiring S
inst✝⁸ : Semiring T
inst✝⁷ : Module R T
inst✝⁶ : Module S T
inst✝⁵ : Module R S
inst✝⁴ : IsScalarTower R S T
inst✝³ : IsScalarTower S T T
inst✝² : FaithfulSMul S T
inst✝¹ : Module.Finite S T
inst✝ : Free R S
H : Module.Finite R S
⊢ finrank R S ≤ finrank R T

Tactic:
have := Module.Finite.trans (R := R) S T
    exact finrank_bot_le_finrank_of_isScalarTower R S T

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := e.symm (u (e 1))
hc : c = e.symm (u (e 1))
x : M
this : ∀ (x : M), x = e.symm x • e 1
⊢ e.symm x • u (e 1) = e.symm x • e.symm (u (e 1)) • e 1

Tactic:
rw [← this]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
⊢ ∀ (r : R),
    (algebraMap R A) r ∈ { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Tactic:
intro r; rw [Algebra.algebraMap_eq_smul_one]; apply s.smul_mem _ h1

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S T U : Subalgebra R A
h✝ : S ≤ T
this : Module ↥S ↥T := (inclusion h✝).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
⊢ ↑x = ↑y

Tactic:
convert! Subtype.ext_iff.mp (h 1) using 1

Goal state after:
case e'_2
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S T U : Subalgebra R A
h✝ : S ≤ T
this : Module ↥S ↥T := (inclusion h✝).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
⊢ ↑x = ↑(x • 1)

case e'_3
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S T U : Subalgebra R A
h✝ : S ≤ T
this : Module ↥S ↥T := (inclusion h✝).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
⊢ ↑y = ↑(y • 1)
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ((RingHom.id A).comp ↑S.val).rangeS = S.toSubsemiring

Tactic:
RingHom.id_comp,

Goal state after:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (↑S.val).rangeS = S.toSubsemiring
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ((RingHom.id A).comp ↑S.val).range = S.toSubring

Tactic:
RingHom.id_comp,

Goal state after:
R : Type u_3
A : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (↑S.val).range = S.toSubring
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
hr₂' : r₂ • ψ ⟨y, ⋯⟩ ∈ R ∙ ψ ⟨y, ⋯⟩
hr₁ : generator (span R {a, ψ ⟨y, ⋯⟩}) = r₁ • a + r₂ • ψ ⟨y, ⋯⟩
⊢ ∃ r₁ r₂, d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩

Tactic:
exact ⟨r₁, r₂, hr₁⟩

Goal state after:
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr✝ : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr' : r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 0
this : {r} ⊆ ↑(closure (↑S \ {r}))
⊢ (fun S ↦ closure ↑S = ⊤) (S \ {r})

Tactic:
simp [Submonoid.closure_sdiff_eq_closure this, hSgen]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
F : Type u_3
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : FunLike F A B
inst✝¹ : MonoidWithZeroHomClass F A B
f : F
inst✝ : IsLocalHom f
inj : Function.Injective ⇑f
hB : IsField B
x y : A
⊢ f x * f y = f y * f x

Tactic:
hB.mul_comm

Goal state after:
A : Type u_1
B : Type u_2
F : Type u_3
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : FunLike F A B
inst✝¹ : MonoidWithZeroHomClass F A B
f : F
inst✝ : IsLocalHom f
inj : Function.Injective ⇑f
hB : IsField B
x y : A
⊢ f y * f x = f y * f x
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
L : Type v
inst✝² : DivisionRing K
inst✝¹ : DivisionRing L
ι : Sort u_1
inst✝ : Nonempty ι
f : K →+* L
s : ι → Subfield K
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective f.injective).image_iInter_eq (s := SetLike.coe ∘ s)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
⊢ (toMatrixAlgEquiv v₁) ((toLinAlgEquiv v₁) M) = M

Tactic:
rw [← Matrix.toLinAlgEquiv_symm, AlgEquiv.symm_apply_apply]

Goal state after:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x y : R
m : ↥M
⊢ x • mk' S y m = mk' S (x * y) m

Tactic:
nth_rw 2 [← one_mul m]

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x y : R
m : ↥M
⊢ x • mk' S y m = mk' S (x * y) (1 * m)
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: case e'_6
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map (↑h) M) S
⊢ inst✝¹ = (((algebraMap R S).comp h.symm.toRingHom).comp h.symm.symm.toRingHom).toAlgebra

Tactic:
RingHom.comp_assoc

Goal state after:
case e'_6
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map (↑h) M) S
⊢ inst✝¹ = ((algebraMap R S).comp (h.symm.toRingHom.comp h.symm.symm.toRingHom)).toAlgebra