mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
⊢ map₂ f (R ∙ m) = map (f m)

Tactic:
by
  funext s
  rw [← span_eq s, map₂_span_span, image2_singleton_left, map_span]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
i : Fin (p.length + 1)
⊢ (p.drop i).last = p.last

Tactic:
simp only [last, drop, Fin.last]

Goal state after:
α : Type u_1
r : SetRel α α
p : RelSeries r
i : Fin (p.length + 1)
⊢ p.toFun ⟨p.length - ↑i + ↑i, ⋯⟩ = p.toFun ⟨p.length, ⋯⟩
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : r.FiniteDimensional
⊢ r.inv.IsWellFounded

Tactic:
by
  rw [IsWellFounded, wellFounded_iff_isEmpty_descending_chain]
  refine ⟨fun ⟨f, hf⟩ ↦ ?_⟩
  let s := RelSeries.mk (r := r) ((RelSeries.longestOf r).length + 1) (f ·) (hf ·)
  exact (RelSeries.longestOf r).length.lt_succ_self.not_ge s.length_le_length_longestOf

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height (f x) ≤ height x

pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height x ≤ height (f x)

Tactic:
· simpa using height_le_height_apply_of_strictMono _ f.symm.strictMono (f x)

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height x ≤ height (f x)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Subsingleton α
⊢ krullDim α ≤ 0

Tactic:
krullDim_nonpos_iff_forall_isMax

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Subsingleton α
⊢ ∀ (x : α), IsMax x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
⊢ 0 < krullDim α ↔ Nontrivial α

Tactic:
by
  rw [← not_subsingleton_iff_nontrivial, ← Order.krullDim_eq_zero_iff_of_orderBot,
    ← ne_eq, ← lt_or_lt_iff_ne, or_iff_right]
  simp [Order.krullDim_nonneg]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
m : M
α : Type u_22
s : Finset α
n : α → N
⊢ m ⊗ₜ[R] ∑ a ∈ s, n a = ∑ a ∈ s, m ⊗ₜ[R] n a

Tactic:
classical
    induction s using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, tmul_add, ih]

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 α
inst✝¹⁰ : LE β
inst✝⁹ : LT β
inst✝⁸ : Zero β
inst✝⁷ : One β
inst✝⁶ : Add β
inst✝⁵ : Mul β
inst✝⁴ : Pow β ℕ
inst✝³ : SMul ℕ β
inst✝² : NatCast β
inst✝¹ : Max β
inst✝ : Bot β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
a b : β
⊢ f (a + b) = f (a ⊔ b)

Tactic:
rw [sup, add, add_eq_sup]

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: m n : ℤ
⊢ IsCoprime m n ↔ m.gcd n = 1

Tactic:
constructor
  · rintro ⟨a, b, h⟩
    refine Nat.dvd_one.mp (Int.gcd_dvd_iff.mpr ⟨a, b, ?_⟩)
    rwa [mul_comm m, mul_comm n, eq_comm]
  · rw [← Int.ofNat_inj, IsCoprime, Int.gcd_eq_gcd_ab, mul_comm m, mul_comm n, Nat.cast_one]
    intro h
    exact ⟨_, _, h⟩

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

Goal state before:
pp: case refine_2
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
r : S
x : M
r_in : r ∈ s
x_in : x ∈ restrictScalars S N
⊢ r • x ∈ ⇑(algebraMap S R) '' s • N

Tactic:
← algebraMap_smul R r

Goal state after:
case refine_2
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
r : S
x : M
r_in : r ∈ s
x_in : x ∈ restrictScalars S N
⊢ (algebraMap S R) r • x ∈ ⇑(algebraMap S R) '' s • N
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: case mpr.inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : Ideal S
h : p.IsPrime
⊢ (⊤.prod p).IsPrime

Tactic:
exact isPrime_ideal_prod_top'

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

Goal state before:
pp: R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
⊢ ∀ ⦃r : R'⦄ ⦃n : M'⦄, r ∈ ↑(Ideal.span s) → n ∈ N → r • n ∈ s • N

Tactic:
rintro r n hr hn

Goal state after:
R' : Type u_1
M' : Type u_2
inst✝² : CommSemiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hr : r ∈ ↑(Ideal.span s)
hn : n ∈ N
⊢ r • n ∈ s • N
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set R
⊢ map f (span s) = span (⇑f '' s)

Tactic:
refine (Submodule.span_eq_of_le _ ?_ ?_).symm

Goal state after:
case refine_1
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set R
⊢ ⇑f '' s ⊆ ↑(map f (span s))

case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set R
⊢ map f (span s) ≤ Submodule.span S (⇑f '' s)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
hf : Function.Bijective ⇑f
K : Ideal S
⊢ (comap f K).IsMaximal ↔ K.IsMaximal

Tactic:
simpa only [isMaximal_def] using! (relIsoOfBijective _ hf).isCoatom_iff _

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

Goal state before:
pp: case h₂
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * (y * gcdB x y)

Tactic:
· rw [mul_left_comm, mul_comm]
    gcongr
    apply hxz.mul_right

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
m : Π₀ (i : ι), M i
i : ι
⊢ (r • m) i = 0 i

Tactic:
exact h i _

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ annihilator R (Π₀ (i : ι), M i) = ⨅ i, annihilator R (M i)

Tactic:
by
  ext r; simp only [mem_annihilator, Ideal.mem_iInf]
  constructor <;> intro h
  · intro i m
    classical simpa using DFunLike.congr_fun (h (DFinsupp.single i m)) i
  · intro m; ext i; exact h i _

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
h : ∀ (i : ι) (m : M i), r • m = 0
m : (i : ι) → M i
i : ι
⊢ (r • m) i = 0 i

Tactic:
exact h i _

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ (x + y * z) / y = x / y + z

Tactic:
by
  rw [eq_comm]
  apply eq_div_of_mul_eq_right h1
  rw [mul_add, EuclideanDomain.mul_div_cancel' h1 h2]

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (z * x + y) / z = x + y / z

Tactic:
by
  rw [eq_comm]
  apply eq_div_of_mul_eq_right h1
  rw [mul_add, EuclideanDomain.mul_div_cancel' h1 h2]

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (x * z + y) / z = x + y / z

Tactic:
rw [mul_comm x z]
  exact mul_add_div_left _ _ _ h1 h2

Goal state after:
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 P : Submodule R M
⊢ ⨅ i, (↑i).annihilator = N.annihilator ⊓ P.annihilator

Tactic:
← iInf_pair,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N P : Submodule R M
⊢ ⨅ i, (↑i).annihilator = ⨅ x ∈ {N, P}, x.annihilator
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
⊢ j ∈ map f '' {J | I ≤ J ∧ J.IsPrime} → j ∈ {J | map f I ≤ J ∧ J.IsPrime}

Tactic:
rintro ⟨J, ⟨hJ, hJ'⟩⟩
    have : J.IsPrime := hJ.right
    exact ⟨hJ' ▸ map_mono hJ.left, hJ' ▸ map_isPrime_of_surjective hf (le_trans h hJ.left)⟩

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

Goal state before:
pp: a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a = b ∨ a = -b

Tactic:
exact Int.natAbs_eq_natAbs_iff

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
hI : I.IsRadical
hJ : J.IsRadical
⊢ (I ⊓ J).radical ≤ I ⊓ J

Tactic:
radical_inf

Goal state after:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
hI : I.IsRadical
hJ : J.IsRadical
⊢ I.radical ⊓ J.radical ≤ I ⊓ J
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case mk.mk
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
toIsCancelMulZero✝¹ : IsCancelMulZero α
gcd✝¹ lcm✝¹ : α → α → α
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
gcd_mul_lcm✝¹ : ∀ (a b : α), Associated (gcd✝¹ a b * lcm✝¹ a b) (a * b)
lcm_zero_left✝¹ : ∀ (a : α), lcm✝¹ 0 a = 0
lcm_zero_right✝¹ : ∀ (a : α), lcm✝¹ a 0 = 0
toIsCancelMulZero✝ : IsCancelMulZero α
gcd✝ lcm✝ : α → α → α
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
gcd_mul_lcm✝ : ∀ (a b : α), Associated (gcd✝ a b * lcm✝ a b) (a * b)
lcm_zero_left✝ : ∀ (a : α), lcm✝ 0 a = 0
lcm_zero_right✝ : ∀ (a : α), lcm✝ a 0 = 0
hgcd : gcd✝¹ = gcd✝
hlcm : lcm✝¹ = lcm✝
⊢ { toIsCancelMulZero := toIsCancelMulZero✝¹, gcd := gcd✝¹, lcm := lcm✝¹, gcd_dvd_left := gcd_dvd_left✝¹,
      gcd_dvd_right := gcd_dvd_right✝¹, dvd_gcd := dvd_gcd✝¹, gcd_mul_lcm := gcd_mul_lcm✝¹,
      lcm_zero_left := lcm_zero_left✝¹, lcm_zero_right := lcm_zero_right✝¹ } =
    { toIsCancelMulZero := toIsCancelMulZero✝, gcd := gcd✝, lcm := lcm✝, gcd_dvd_left := gcd_dvd_left✝,
      gcd_dvd_right := gcd_dvd_right✝, dvd_gcd := dvd_gcd✝, gcd_mul_lcm := gcd_mul_lcm✝,
      lcm_zero_left := lcm_zero_left✝, lcm_zero_right := lcm_zero_right✝ }

Tactic:
simp only [hgcd, hlcm]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
u : αˣ
a✝ : Nontrivial α
⊢ (if ↑u = 0 then 1 else Classical.choose ⋯) = u⁻¹

Tactic:
simp_rw [if_neg (Units.ne_zero u), Units.ext_iff]

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
u : αˣ
a✝ : Nontrivial α
⊢ ↑(Classical.choose ⋯) = ↑u⁻¹
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ (∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f) ↔
    ∀ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), ¬Injective ⇑f

Tactic:
← not_iff_not

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ (¬∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f) ↔
    ¬∀ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), ¬Injective ⇑f
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 b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
⊢ normalize (Classical.choose ⋯) ∣ a

Tactic:
normalize_dvd_iff,

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 b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
⊢ Classical.choose ⋯ ∣ a
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 b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
⊢ normalize (Classical.choose ⋯) ∣ b

Tactic:
normalize_dvd_iff,

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 b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
⊢ Classical.choose ⋯ ∣ b
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
β : Type w
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
⊢ (diagonal d).map f = diagonal fun m ↦ f (d m)

Tactic:
ext
  simp only [diagonal_apply, map_apply]
  split_ifs <;> simp [h]

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

Goal state before:
pp: case neg.inl.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ (↑(f i) ∪ ⋃ x ∈ ↑t, ↑(f x))
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : ¬f b ≤ f i
Hi : ¬I ≤ f i
this : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i
r : R
hri : r ∉ ↑(f i)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ¬↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
s : R
hsI : s ∈ ↑I
hs : s ∉ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
hsi : s ∈ f i
hb : r + s ∈ ↑(f b)
⊢ False

Tactic:
exact hs (Or.inl <| Or.inr <| add_sub_cancel_left r s ▸ (f b).sub_mem hb hrb)

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

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

Tactic:
← not_iff_not

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.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d : n → α
M : Matrix m n α
i : m
j : n
⊢ (M * diagonal d) i j = M i j * d j

Tactic:
by
  rw [← diagonal_transpose]
  apply dotProduct_diagonal

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a b : Ideal R
hp : ∀ I ∈ S, I ≠ a → I ≠ b → I.IsPrime
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ ↑M ⊆ ⋃ I ∈ S, ↑I ↔ M ∈ S

Tactic:
refine (subset_union_prime_finite hs a b hp).trans ⟨fun ⟨I, mem, le⟩ ↦ ?_, (⟨M, ·, le_rfl⟩)⟩

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a b : Ideal R
hp : ∀ I ∈ S, I ≠ a → I ≠ b → I.IsPrime
ha : a ≠ ⊤
hb : b ≠ ⊤
x✝ : ∃ i ∈ S, M ≤ i
I : Ideal R
mem : I ∈ S
le : M ≤ I
⊢ M ∈ S
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun a b ↦ ↑(if h : b ∈ I then ⟨b, h⟩ else 0) • v a) = a.sum fun i c ↦ c • v i

Tactic:
apply Finsupp.sum_congr
      intro i _
      rw [dif_pos (ha i)]

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f✝ : C →ₐ[A] D
f : B → D
map_one'✝¹ : f 1 = 1
map_mul'✝¹ :
  ∀ (x y : B),
    { toFun := f, map_one' := map_one'✝¹ }.toFun (x * y) =
      { toFun := f, map_one' := map_one'✝¹ }.toFun x * { toFun := f, map_one' := map_one'✝¹ }.toFun y
map_zero'✝¹ : (↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun 0 = 0
map_add'✝¹ :
  ∀ (x y : B),
    (↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun (x + y) =
      (↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun x +
        (↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun y
commutes'✝ :
  ∀ (r : A),
    (↑↑{ toFun := f, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹,
                map_add' := map_add'✝¹ }).toFun
        ((algebraMap A B) r) =
      (algebraMap A D) r
g : C → D
map_one'✝ : g 1 = 1
map_mul'✝ :
  ∀ (x y : C),
    { toFun := g, map_one' := map_one'✝ }.toFun (x * y) =
      { toFun := g, map_one' := map_one'✝ }.toFun x * { toFun := g, map_one' := map_one'✝ }.toFun y
map_zero'✝ : (↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun 0 = 0
map_add'✝ :
  ∀ (x y : C),
    (↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun (x + y) =
      (↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun x +
        (↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun y
hg :
  ∀ (r : B),
    (↑↑{ toFun := g, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝,
                map_add' := map_add'✝ }).toFun
        ((algebraMap B C) r) =
      (algebraMap B D) r
⊢ f = fun x ↦ g ((algebraMap B C) x)

Tactic:
by
      ext x
      exact (hg x).symm

Goal state after:
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_3
β : Type 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⟩
hS : iUnion S = univ
t : Set β
⊢ (iUnionLift S f hf univ ⋯ ∘ fun a ↦ ⟨a, ⋯⟩) ⁻¹' t = ⋃ i, Subtype.val '' f i ⁻¹' t

Tactic:
preimage_comp,

Goal state after:
α : Type u_1
ι : Sort u_3
β : Type 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⟩
hS : iUnion S = univ
t : Set β
⊢ (fun a ↦ ⟨a, ⋯⟩) ⁻¹' iUnionLift S f hf univ ⋯ ⁻¹' t = ⋃ i, Subtype.val '' f i ⁻¹' t
Module: Mathlib.Algebra.Algebra.Subalgebra.Tower

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
I : Ideal A
⊢ Disjoint 1 (Submodule.restrictScalars (↥S) I) ↔ Disjoint (toSubmodule S) (Submodule.restrictScalars R I)

Tactic:
by
  simp [← Submodule.disjoint_restrictScalars_iff R]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : Module R A
S T : NonUnitalSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
rw [← mem_toNonUnitalSubring, ← mem_toNonUnitalSubring, h]

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ Disjoint (A i) (A j) ∧ A i ⊔ A j = ⊤ ↔ IsCompl (A i) (A j)

Tactic:
exact ⟨fun ⟨hd, ht⟩ ↦ ⟨hd, codisjoint_iff.mpr ht⟩, fun ⟨hd, ht⟩ ↦ ⟨hd, ht.eq_top⟩⟩

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i ↦ A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
i : ↑s
m : M
⊢ m ∈ p ⊓ A ↑i ↔ m ∈ ↑⟨A ↑i, ⋯⟩

Tactic:
inf_of_le_right (hp i i.property)

Goal state after:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i ↦ A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
i : ↑s
m : M
⊢ m ∈ A ↑i ↔ m ∈ ↑⟨A ↑i, ⋯⟩
Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommSemiring R
S : Type u_1
inst✝⁹ : Semiring S
inst✝⁸ : Algebra R S
ι₁ : Type v₁
ι₂ : Type v₂
inst✝⁷ : DecidableEq ι₁
inst✝⁶ : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₂ : ι₂ → Type w₂
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
i₁ : ι₁
m₁ : M₁ i₁
i₂ : ι₂
m₂ : M₂ i₂
⊢ (TensorProduct.directSum R S M₁ M₂).symm ((lof S (ι₁ × ι₂) (fun i ↦ M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)) =
    (lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (lof R ι₂ M₂ i₂) m₂

Tactic:
by
  rw [LinearEquiv.symm_apply_eq, directSum_lof_tmul_lof]

Goal state after: