mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
⊢ IsRightRegular A ↔ Function.Injective fun v ↦ v ᵥ* A

Tactic:
cases isEmpty_or_nonempty m

Goal state after:
case inl
m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
h✝ : IsEmpty m
⊢ IsRightRegular A ↔ Function.Injective fun v ↦ v ᵥ* A

case inr
m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
h✝ : Nonempty m
⊢ IsRightRegular A ↔ Function.Injective fun v ↦ v ᵥ* A
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : Multiset.map g (toMultiset f) = toMultiset (mapDomain g f)
⊢ Multiset.map g (n • {a}) + toMultiset (mapDomain g f) = n • {g a} + toMultiset (mapDomain g f)

Tactic:
← Multiset.coe_mapAddMonoidHom,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : Multiset.map g (toMultiset f) = toMultiset (mapDomain g f)
⊢ (Multiset.mapAddMonoidHom g) (n • {a}) + toMultiset (mapDomain g f) = n • {g a} + toMultiset (mapDomain g f)
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₁ a b
⊢ t₂ a b

pp: case refine_2
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₂ a b
⊢ t₁ a b

Tactic:
· have H' : a - b ∈ {x | t₁ x 0} := sub_self b ▸ t₁.sub H (t₁.refl b)
      rw [h] at H'
      convert! t₂.add H' (t₂.refl b) using 1 <;> abel

Goal state after:
case refine_2
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₂ a b
⊢ t₁ a b
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Free R M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : Free R M'
inst✝² : OrzechProperty R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
f : M →ₗ[R] M'
hf : Surjective ⇑f
h : finrank R M ≤ finrank R M'
⊢ Bijective ⇑f

Tactic:
by
  cases subsingleton_or_nontrivial R
  -- TODO : figure out how to make `nontriviality` work here nicely
  · have := Module.subsingleton R M
    exact ⟨Function.injective_of_subsingleton f, hf⟩
  rcases finrank_le_iff_exists_linearMap.mp h with ⟨_, hi⟩
  exact OrzechProperty.bijective_of_surjective_of_injective _ _ hi hf

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, u = c • LinearMap.id

Tactic:
set c := e.symm (u (e 1)) with hc

Goal state after:
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))
⊢ ∃! c, u = c • LinearMap.id
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
⊢ b ∈ {x | ∃ m ∈ M, m * x ∈ s} → a * b ∈ {x | ∃ m ∈ M, m * x ∈ s}

Tactic:
⟨n, hn, hb⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
⊢ a * b ∈ {x | ∃ m ∈ M, m * x ∈ s}
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
⊢ b ∈ {x | ∃ m ∈ M, m * x ∈ s} → a + b ∈ {x | ∃ m ∈ M, m * x ∈ s}

Tactic:
⟨n, hn, hb⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
⊢ a + b ∈ {x | ∃ m ∈ M, m * x ∈ s}
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
⊢ x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure ∅) ↔ x = 0

Tactic:
NonUnitalSubsemiring.closure_empty,

Goal state after:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
⊢ x ∈ Submodule.span R ↑⊥ ↔ x = 0
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ⇑f
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : f ∘ₗ g₁ = inl R P Q
⊢ ∃ h, f ∘ₗ h = LinearMap.id

Tactic:
rcases projective_lifting_property f (.inr _ _ _) hf with ⟨g₂, hg₂⟩

Goal state after:
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ⇑f
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : f ∘ₗ g₁ = inl R P Q
g₂ : Q →ₗ[R] P × Q →₀ R
hg₂ : f ∘ₗ g₂ = inr R P Q
⊢ ∃ h, f ∘ₗ h = LinearMap.id
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : Algebra R S
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
ι : Type u_5
inst✝ : DecidableEq ι
m : M
p : ι →₀ R
i : ι
⊢ ((finsuppScalarRight R S M ι) (m ⊗ₜ[R] p)) i = p i • m

Tactic:
simp [finsuppScalarRight]

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

Goal state before:
pp: R : Type u_8
S : Type u_9
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module S N
σ : R →+* S
σ' : S →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst✝ : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
g : N →ₗ[S] N →₀ S :=
  { toFun := fun x ↦ mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm x))), map_add' := ⋯, map_smul' := ⋯ }
⊢ Projective S N

Tactic:
refine ⟨⟨g, fun x ↦ ?_⟩⟩

Goal state after:
R : Type u_8
S : Type u_9
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module S N
σ : R →+* S
σ' : S →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst✝ : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
g : N →ₗ[S] N →₀ S :=
  { toFun := fun x ↦ mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm x))), map_add' := ⋯, map_smul' := ⋯ }
x : N
⊢ (linearCombination S id) (g x) = x
Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct

Goal state before:
pp: case add
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
i : ι₁
x y : M₁ i ⊗[R] M₂'
h₁ : (directSumLeft R S M₁ M₂').symm ((of (fun i ↦ M₁ i ⊗[R] M₂') i) x) = (rTensor M₂' (lof R ι₁ M₁ i)) x
h₂ : (directSumLeft R S M₁ M₂').symm ((of (fun i ↦ M₁ i ⊗[R] M₂') i) y) = (rTensor M₂' (lof R ι₁ M₁ i)) y
⊢ (directSumLeft R S M₁ M₂').symm ((of (fun i ↦ M₁ i ⊗[R] M₂') i) (x + y)) = (rTensor M₂' (lof R ι₁ M₁ i)) (x + y)

Tactic:
| add x y h₁ h₂ =>

Goal state after:
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: A : Type u_2
a : A
inst✝¹ : Semiring A
inst✝ : StarRing A
ha : IsSelfAdjoint a
⊢ IsSelfAdjoint a⁻¹ʳ

Tactic:
rw [isSelfAdjoint_iff, ← Ring.inverse_star, ha.star_eq]

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

Goal state before:
pp: case hl.fst
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(selfAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑x + (skewAdjoint.submodule R A).subtype 0)).1 = ↑x

Tactic:
Submodule.coe_subtype

Goal state after:
case hl.fst
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(selfAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑x + ↑0)).1 = ↑x
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: case hl.snd
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(selfAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑x + (skewAdjoint.submodule R A).subtype 0)).2 = 0

Tactic:
Submodule.coe_subtype

Goal state after:
case hl.snd
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(selfAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑x + ↑0)).2 = 0
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: case hr.fst
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(skewAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑0 + (skewAdjoint.submodule R A).subtype x)).1 = 0

Tactic:
Submodule.coe_subtype

Goal state after:
case hr.fst
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(skewAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑0 + ↑x)).1 = 0
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: case hr.snd
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(skewAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑0 + (skewAdjoint.submodule R A).subtype x)).2 = ↑x

Tactic:
Submodule.coe_subtype

Goal state after:
case hr.snd
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(skewAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑0 + ↑x)).2 = ↑x
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Star A
inst✝⁸ : Semiring B
inst✝⁷ : Algebra R B
inst✝⁶ : Star B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Star C
inst✝² : Semiring D
inst✝¹ : Algebra R D
inst✝ : Star D
f : B →⋆ₐ[R] C
g : A →⋆ₐ[R] B
⊢ ∀ (x : A), (↑↑((↑f).comp ↑g).toRingHom).toFun (star x) = star ((↑↑((↑f).comp ↑g).toRingHom).toFun x)

Tactic:
by
      simp only [map_star, AlgHom.toFun_eq_coe, AlgHom.coe_comp, coe_toAlgHom,
        Function.comp_apply, forall_const]

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

Goal state before:
pp: case succ
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M ≃ₗ[R] M
n : ℕ
h : LinearEquiv.baseChange R A M M (f ^ n) = LinearEquiv.baseChange R A M M f ^ n
⊢ LinearEquiv.baseChange R A M M (f ^ (n + 1)) = LinearEquiv.baseChange R A M M f ^ (n + 1)

Tactic:
| succ n h =>

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

Goal state before:
pp: case succ
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M ≃ₗ[R] M
n : ℕ
h : LinearEquiv.baseChange R A M M (f ^ ↑n) = LinearEquiv.baseChange R A M M f ^ ↑n
⊢ LinearEquiv.baseChange R A M M (f ^ (↑n + 1)) = LinearEquiv.baseChange R A M M f ^ (↑n + 1)

Tactic:
| succ n h =>

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

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
⊢ Nontrivial (OreLocalization S R) ↔ ¬0 ∈ S

Tactic:
← not_subsingleton_iff_nontrivial,

Goal state after:
R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
⊢ ¬Subsingleton (OreLocalization S R) ↔ ¬0 ∈ S
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r r' : X
s : ↥S
⊢ r /ₒ s + r' /ₒ s = (r + r') /ₒ s

Tactic:
by
  simp [oreDiv_add_char s s 1 1 (by simp)]

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

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
s : Set K
p : (x : K) → x ∈ closure s → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : x ∈ closure s), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : x ∈ closure s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯
x : K
h : x ∈ closure s
⊢ ∀ x ∈ {x | ∃ (hx : x ∈ closure s), p x hx}, x⁻¹ ∈ {x | ∃ (hx : x ∈ closure s), p x hx}

Tactic:
rintro _ ⟨_, hx⟩; exact ⟨_, inv _ _ hx⟩

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

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : K
s : Subfield K :=
  let __spread.0 := (⨆ i, (S i).toSubring).copy (⋃ i, ↑(S i).toSubring) ⋯;
  { toSubring := __spread.0, inv_mem' := ⋯ }
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
have : iSup S = s := le_antisymm
    (iSup_le fun i ↦ le_iSup (fun i ↦ (S i : Set K)) i) (Set.iUnion_subset fun _ ↦ le_iSup S _)

Goal state after:
K : Type u
inst✝ : DivisionRing K
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : K
s : Subfield K :=
  let __spread.0 := (⨆ i, (S i).toSubring).copy (⋃ i, ↑(S i).toSubring) ⋯;
  { toSubring := __spread.0, inv_mem' := ⋯ }
this : iSup S = s
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
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₁
i j : n
⊢ (toMatrix v₁ v₁) id i j = 1 i j

Tactic:
simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
l : Type u_2
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Fintype l
inst✝ : DecidableEq l
b : Basis l R M₁
b' : Basis l R M₂
i j : l
⊢ (toMatrix b' b) (↑(b'.equiv b (Equiv.refl l))) i j = 1 i j

Tactic:
simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
h : 0 ∉ S
⊢ Nontrivial N

Tactic:
← not_subsingleton_iff_nontrivial,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
h : 0 ∉ S
⊢ ¬Subsingleton N
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
S : Submonoid M
p : Type u_4
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d
⊢ (mk 0 1).liftOn f H = f 0 1

Tactic:
liftOn_mk

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
S : Submonoid M
p : Type u_4
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d
⊢ f 0 1 = f 0 1
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationMap N
inst✝ : IsCancelMulZero M
⊢ IsCancelMulZero N

Tactic:
simp_rw [isCancelMulZero_iff_forall_isRegular, Commute.isRegular_iff (Commute.all _),
    ← Commute.isRightRegular_iff (Commute.all _)]
  intro n hn
  have ⟨ms, eq⟩ := f.surj n
  refine (eq ▸ f.map_isRegular (isCancelMulZero_iff_forall_isRegular.mp ‹_› ?_)).2.of_mul
  refine fun h ↦ hn ?_
  rwa [h, map_zero, (f.map_units _).mul_left_eq_zero] at eq

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝³ : Fintype m
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₁
⊢ ((toLin v₂ v₁) M') (((toLin v₁ v₂) M) x) = x

Tactic:
← Matrix.toLin_mul_apply,

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝³ : Fintype m
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₁
⊢ ((toLin v₁ v₁) (M' * M)) x = x
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝³ : Fintype m
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₂
⊢ ((toLin v₁ v₂) M) (((toLin v₂ v₁) M') x) = x

Tactic:
← Matrix.toLin_mul_apply,

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝³ : Fintype m
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₂
⊢ ((toLin v₂ v₂) (M * M')) x = x
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
S : Submonoid R
inst✝⁴ : OreSet S
X : Type u_2
inst✝³ : AddCommMonoid X
inst✝² : Module R X
R₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
x : OreLocalization S R
⊢ r • x = (numeratorRingHom.comp (algebraMap R₀ R)) r * x

Tactic:
dsimp
    rw [Algebra.algebraMap_eq_smul_one, ← smul_eq_mul, smul_one_oreDiv_one_smul]

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.e_a.e_a
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑s₁ = r₃ * ↑s₂
⊢ ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * f r₃ = ↑(fS s₂)⁻¹

Tactic:
norm_cast at h₃

Goal state after:
case c.c.e_a.e_a
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑(s₃ * s₁) = r₃ * ↑s₂
⊢ ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * f r₃ = ↑(fS s₂)⁻¹
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case surj
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
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : ↥M
e : h.symm y * (algebraMap R S) ↑(x, s).2 = (algebraMap R S) (x, s).1
⊢ ∃ x, y * (algebraMap R P) ↑x.2 = (algebraMap R P) x.1

Tactic:
apply_fun (show S → P from h) at e

Goal state after:
case surj
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
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : ↥M
e :
  (have this := ⇑h;
      this)
      (h.symm y * (algebraMap R S) ↑(x, s).2) =
    (have this := ⇑h;
      this)
      ((algebraMap R S) (x, s).1)
⊢ ∃ x, y * (algebraMap R P) ↑x.2 = (algebraMap R P) x.1
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hx : x ∈ K⁰
⊢ x ∈ IsUnit.submonoid K

Tactic:
have ⟨r, eq⟩ := surj R⁰ x

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hx : x ∈ K⁰
r : R × ↥R⁰
eq : x * (algebraMap R K) ↑r.2 = (algebraMap R K) r.1
⊢ x ∈ IsUnit.submonoid K
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ K⁰ = IsUnit.submonoid K

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (isUnit_le_nonZeroDivisors K)
  have ⟨r, eq⟩ := surj R⁰ x
  let r' : R⁰ := ⟨r.1, mem_nonZeroDivisors_of_injective (IsFractionRing.injective R K)
    (eq ▸ mul_mem hx (map_units ..).mem_nonZeroDivisors)⟩
  exact isUnit_of_mul_isUnit_left <| eq ▸ map_units K r'

Goal state after: