mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
a : α
⊢ a ∣ gcd 0 ↔ ∀ (b : α), b ∈ 0 → a ∣ b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ normalize (gcd 0) = gcd 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
x✝ : normalize s.gcd = s.gcd
⊢ normalize (a ::ₘ s).gcd = (a ::ₘ s).gcd

Tactic:
simp

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

Goal state before:
pp: case mpr.refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ (∀ (x : α), x ∈ 0 → x = 0) → gcd 0 = 0

Tactic:
simp

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

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
⊢ ∀ b ∈ map f '' A, map f (sInf A) ≤ b

Tactic:
intro j

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective ⇑f
h : ∀ J ∈ A, RingHom.ker f ≤ J
j : Ideal S
⊢ j ∈ map f '' A → map f (sInf A) ≤ j
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s : Multiset α
⊢ (dedup 0).gcd = gcd 0

Tactic:
simp

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

Goal state before:
pp: case inl
h : 0 ≤ 0
⊢ normalize 0 = -0

Tactic:
simp

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

Goal state before:
pp: case refine_2
n : ℕ
⊢ (fun x ↦ x.out.natAbs) ((fun x ↦ Associates.mk ↑x) n) = n

Tactic:
dsimp only [Associates.out_mk]

Goal state after:
case refine_2
n : ℕ
⊢ (normalize ↑n).natAbs = n
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : Nontrivial α
⊢ s.lcm f = 0 ↔ ∃ x ∈ s, f x = 0

Tactic:
simp only [lcm_def, Multiset.lcm_eq_zero_iff, Multiset.mem_map, mem_val]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
m : Multiset R
⊢ (Multiset.map (fun x ↦ span {x}) 0).prod = span {Multiset.prod 0}

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → R
hI : (↑s).Pairwise (IsCoprime on I)
x : R
⊢ (x ∈ s.inf fun i ↦ span {I i}) ↔ x ∈ span {∏ i ∈ s, I i}

Tactic:
simp only [Submodule.mem_finsetInf, Ideal.mem_span_singleton]

Goal state after:
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → R
hI : (↑s).Pairwise (IsCoprime on I)
x : R
⊢ (∀ i ∈ s, I i ∣ x) ↔ ∏ i ∈ s, I i ∣ x
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case empty
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ ∅.gcd f = 0 ↔ ∀ x ∈ ∅, f x = 0

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
φ : B →+* C
⊢ (fun g ↦ f.liftOfRightInverseAux f_inv hf ↑g ⋯) ((fun φ ↦ ⟨φ.comp f, ⋯⟩) φ) = φ

Tactic:
ext b

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
φ : B →+* C
b : B
⊢ ((fun g ↦ f.liftOfRightInverseAux f_inv hf ↑g ⋯) ((fun φ ↦ ⟨φ.comp f, ⋯⟩) φ)) b = φ b
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ {x ∈ s | f x ≠ 0}.gcd f = {x ∈ s | f x ≠ 0}.gcd f

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
h : B →+* C
hh : h.comp f = g
⊢ h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩

Tactic:
simp_rw [← hh]
  exact ((f.liftOfRightInverse f_inv hf).apply_symm_apply _).symm

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

Goal state before:
pp: case refine_2.refine_1
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidablePred fun x ↦ f x = 0
⊢ {x ∈ ∅ | f x = 0}.gcd f = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Semiring S
inst✝ : Algebra R S
I : Ideal R
x y : ↥I
⊢ ↑((idealMap S I) (x * y)) = ↑((idealMap S I) x * (idealMap S I) y)

Tactic:
simp

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

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
x✝ : R
⊢ x✝ ∈ RingHom.ker (algebraMap R A) ↔ x✝ ∈ ⊥

Tactic:
simp

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

Goal state before:
pp: case refine_1
β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∅.gcd fun x ↦ a * f x) = normalize a * ∅.gcd f

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ Associated (∅.gcd fun x ↦ a * f x) (a * ∅.gcd f)

Tactic:
simp

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
⊢ (if 1 = 1 then 1 else Quotient.out 1) = 1

Tactic:
simp

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

Goal state before:
pp: case e'_2
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
u : αˣ
a✝ : Nontrivial α
⊢ normUnit ↑u = normUnit (1 * ↑u)

Tactic:
simp

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

Goal state before:
pp: case e'_3
α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
u : αˣ
a✝ : Nontrivial α
⊢ u⁻¹ = u⁻¹ * normUnit 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
a : Associates α
⊢ ∀ (a : α), Associates.out ⟦a⟧ = 0 ↔ ⟦a⟧ = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MonoidWithZero α
inst✝ : NormalizationMonoid α
⊢ Associates.out 0 = 0

Tactic:
simp

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

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
a : α
⊢ (∀ x ∈ ∅, a ∣ f x - g x) → GCDMonoid.gcd a (∅.gcd f) = GCDMonoid.gcd a (∅.gcd g)

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
y : α
⊢ normalize (0 * y) = normalize 0 * normalize y

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ [IsCoprime I J, IsCoprime I J, IsCoprime I J, IsCoprime I J, IsCoprime I J].TFAE

Tactic:
simp

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizationMonoid α
x : α
hx : x ≠ 0
⊢ normalize (x * 0) = normalize x * normalize 0

Tactic:
simp

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

Goal state before:
pp: case empty
ι : Type u_1
s : Finset ι
f : ι → ℤ
⊢ 0 ≤ ∅.gcd f

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a : α
⊢ Associated (gcd 1 a) 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a : α
⊢ Associated (gcd a 1) 1

Tactic:
simp

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

Goal state before:
pp: case empty
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
J : ι → Ideal R
hp : (↑∅).Pairwise (IsCoprime on J)
⊢ ∏ i ∈ ∅, J i = ⨅ i ∈ ∅, J i

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
b c : α
⊢ gcd (0 * b) (0 * c) = normalize 0 * gcd b c

Tactic:
simp

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

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
s : Finset ι
J : ι → Ideal R
hp : (↑s).Pairwise (IsCoprime on J)
⊢ ∏ i ∈ s, J i = ⨅ i ∈ s, J i

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert a s hs ih =>
    simp_all only [Finset.iInf_insert, Finset.coe_insert, Set.pairwise_insert, SetLike.mem_coe,
      ne_eq, not_false_eq_true, Finset.prod_insert, forall_const]
    obtain ⟨hp1, hp2⟩ := hp
    rw [Ideal.mul_eq_inf_of_isCoprime (isCoprime_biInf (by grind))]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
n : α
a✝ : GCDMonoid α
H : 0 ∣ 0 * n
⊢ 0 = 0 * n

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ gcd d₁ b ^ k ∣ 1

Tactic:
apply IsUnit.dvd
      apply IsUnit.pow
      apply isUnit_of_dvd_one
      grw [hd₁, hab.dvd]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
x✝ : 1 ≠ 0
⊢ (I ^ 1).radical = I.radical

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
⊢ lcm a b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
b c : α
⊢ lcm (0 * b) (0 * c) = normalize 0 * lcm b c

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n : α
⊢ m ∣ m * n

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n : α
⊢ n ∣ m * n

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a b = gcd a c

Tactic:
gcd_eq_of_dvd_sub_right h

Goal state after:
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a c = gcd a c
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a b : α
h✝ : a = 0
⊢ normalize 0 = 0

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a b : α
h✝ : ¬a = 0
⊢ normalize (normalize (Classical.choose ⋯)) = normalize (Classical.choose ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : OrzechProperty R
n : ℕ
i : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hi : Injective ⇑i
x✝ : Fin n
⊢ (LinearMap.funLeft R R Fin.castSucc) 0 x✝ = (LinearMap.funLeft R R Fin.castSucc) (update 0 (Fin.last n) 1) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⊥ = R ∙ 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : IsBezout R
x y : R
⊢ Ideal.span ↑{x, y} = Ideal.span {x, y}

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ x ∈ {x, y}

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ y ∈ {x, y}

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ gcd x y ∈ {gcd x y}

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case empty
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
⊢ ∃ g, ∅.gcd f = ∑ a ∈ ∅, f a * g a

Tactic:
simp

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

Goal state before:
pp: case neg
α : 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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ a * d ∣ c * d

Tactic:
mul_dvd_mul_iff_right h_1.2

Goal state after:
case neg
α : 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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ a ∣ c
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
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
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ a * d ∣ c * d

Tactic:
mul_dvd_mul_iff_right h_1.2

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
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
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ a ∣ c
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
u : G₀ˣ
⊢ (if h : ↑u = 0 then 1 else (Units.mk0 (↑u) h)⁻¹) = u⁻¹

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝ : Add α
M N : Matrix m n α
i✝ : n
j✝ : m
⊢ (M + N)ᵀ i✝ j✝ = (Mᵀ + Nᵀ) i✝ j✝

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝ : Sub α
M N : Matrix m n α
i✝ : n
j✝ : m
⊢ (M - N)ᵀ i✝ j✝ = (Mᵀ - Nᵀ) i✝ j✝

Tactic:
simp

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

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
eₘ : m ≃ l
eₙ : n ≃ o
M : Matrix m n α
⊢ (fun M ↦ M.submatrix ⇑eₘ ⇑eₙ) ((fun M ↦ M.submatrix ⇑eₘ.symm ⇑eₙ.symm) M) = M

Tactic:
simp

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

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
eₘ : m ≃ l
eₙ : n ≃ o
M : Matrix l o α
⊢ (fun M ↦ M.submatrix ⇑eₘ.symm ⇑eₙ.symm) ((fun M ↦ M.submatrix ⇑eₘ ⇑eₙ) M) = M

Tactic:
simp

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ lift.{w, v} ↑(Fintype.card ↑J) = lift.{v, w} ↑(Fintype.card ↑J)

Tactic:
simp

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ⊆ ↑(span R w)
⊢ Fintype.card ι ≤ Fintype.card ↑w

Tactic:
fapply card_le_of_injective' R
  · apply Finsupp.linearCombination
    exact fun i => Span.repr R w ⟨v i, s (mem_range_self i)⟩
  · intro f g h
    apply_fun linearCombination R ((↑) : w → M) at h
    simp only [linearCombination_linearCombination,
               Span.finsupp_linearCombination_repr] at h
    exact i h

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
b✝ : Basis β R (β →₀ R) := { repr := 1 }
a : α
b : β
⊢ (((linearCombination R fun i ↦ f (single i 1)) ∘ₗ lsingle a) 1) b = ((f ∘ₗ lsingle a) 1) b

Tactic:
simp

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ #ι = Module.rank R M

Tactic:
Module.rank_def

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ #ι = ⨆ ι, #↑↑ι
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
x✝ : ↑(range ⇑v)
⊢ id ↑x✝ = v.reindexRange x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
⊢ Module.rank R R = ↑1

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
hbt : b ∉ t
⊢ ∀ j ∈ t, (f j).IsPrime

Tactic:
intro j

Goal state after:
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
hbt : b ∉ t
j : ι
⊢ j ∈ t → (f j).IsPrime
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case hc
R : Type u
S : Type u_1
M : Type v
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ Module.rank S M < ℵ₀

pp: case hd
R : Type u
S : Type u_1
M : Type v
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ Module.rank R M < ℵ₀

Tactic:
· exact lt_of_le_of_lt (rank_top_le_rank_of_isScalarTower R S M) (Module.rank_lt_aleph0 R M)

Goal state after:
case hd
R : Type u
S : Type u_1
M : Type v
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : Module.Finite R M
inst✝⁵ : Semiring S
inst✝⁴ : Module S M
inst✝³ : Module R S
inst✝² : IsScalarTower R S S
inst✝¹ : FaithfulSMul R S
inst✝ : IsScalarTower R S M
⊢ Module.rank R M < ℵ₀
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case e'_4
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : ∃ n f, Injective ⇑f
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
inj : Injective ⇑f
g : (ℕ →₀ R) →ₗ[R] Fin n → R
hg : Injective ⇑g
⊢ Module.rank R (Fin n → R) = Cardinal.lift.{0, u} (Module.rank R (Fin n → R))

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ StrongRankCondition R ↔ ∀ n > 0, 0 < finrank R (Fin n → R)

Tactic:
strongRankCondition_iff_forall_rank_lt_aleph0,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (∀ (n : ℕ), Module.rank R (Fin n → R) < ℵ₀) ↔ ∀ n > 0, 0 < finrank R (Fin n → R)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert b t), ↑(f i)
has : a ∉ insert b t
hbs : b ∈ insert b t
⊢ ∀ j ∈ t, (f j).IsPrime

Tactic:
intro j

Goal state after:
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert b t), ↑(f i)
has : a ∉ insert b t
hbs : b ∈ insert b t
j : ι
⊢ j ∈ t → (f j).IsPrime
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case e'_3
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
⊢ v i * w i = diagonal v i i * w i

Tactic:
simp

Goal state after: