mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : CompleteSpace F
inst✝² : LocallyCompactSpace 𝕜
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
p : α × 𝕜
A : deriv (f p.1) p.2 ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (range (f p.1)))
⊢ range (f p.1) ⊆ range (Function.uncurry f)

Tactic:
rintro - ⟨x, rfl⟩

Goal state after:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : CompleteSpace F
inst✝² : LocallyCompactSpace 𝕜
inst✝¹ : MeasurableSpace 𝕜
inst✝ : OpensMeasurableSpace 𝕜
h : SecondCountableTopologyEither α F
f : α → 𝕜 → F
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
hα : SecondCountableTopology α
this : ProperSpace 𝕜
p : α × 𝕜
A : deriv (f p.1) p.2 ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (range (f p.1)))
x : 𝕜
⊢ f p.1 x ∈ range (Function.uncurry f)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case e'_3
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn (fun t ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ t ∈ Icc 0 1, HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : ℝ → 𝕜 := fun t ↦ z₀ + t • z₁
hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1
hderiv' : ∀ t ∈ [[0, 1]], HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t
⊢ f (z₀ + z₁) - f z₀ = (f ∘ γ) 1 - (f ∘ γ) 0

Tactic:
simp only [γ, Function.comp_apply, one_smul, zero_smul, add_zero]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
⊢ ∫ (a : ℝ) in t..t + T, f ↑a = ∫ (b : AddCircle T), f b

Tactic:
rw [integral_of_le, AddCircle.integral_preimage T t f]

Goal state after:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
⊢ t ≤ t + T
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
h₁f : Periodic f T
hT : T ≠ 0
h₂f : IntervalIntegrable f volume 0 T
a₁ a₂ : ℝ
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
apply h₁f.intervalIntegrable hT (t := 0)
  simpa

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case inl
α : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
a b : ℝ
f : ℝ → α → E
hab : a ≤ b
h_int : Integrable (uncurry f) ((volume.restrict (Ioc a b)).prod μ)
⊢ ∫ (x : ℝ) in Ioc a b, ∫ (y : α), f x y ∂μ ∂volume = ∫ (y : α), ∫ (x : ℝ) in Ioc a b, f x y ∂volume ∂μ

Tactic:
exact integral_integral_swap h_int

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
⊢ p.natDegree ∣ finrank F p.SplittingField

Tactic:
have hp : p.degree ≠ 0 := fun h =>
    Nat.Prime.ne_zero p_deg (natDegree_eq_zero_iff_degree_le_zero.mpr (le_of_eq h))

Goal state after:
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
⊢ p.natDegree ∣ finrank F p.SplittingField
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.esymm (s.card - k) = ∑ x ∈ Finset.range (s.card + 1), if k = s.card - x then s.esymm x else 0

Tactic:
rw [Finset.sum_eq_single_of_mem (Multiset.card s - k) _] <;> grind

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist x y < dist y z
⊢ max (dist x y) (dist y z) ≤ dist x z

Tactic:
rw [max_eq_right h.le]

Goal state after:
case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist x y < dist y z
⊢ dist y z ≤ dist x z
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case pos
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖

Tactic:
have h_bd : BddAbove (Set.range fun i ↦ ‖f i‖) :=
    h.tendsto_cofinite_one.norm'.bddAbove_range_of_cofinite

Goal state after:
case pos
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
h_bd : BddAbove (Set.range fun i ↦ ‖f i‖)
⊢ ‖∏' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case h₀.a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsRight R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff y) x = (coeff y) 0
u snd✝ : σ →₀ ℕ
huv : (u, snd✝) ∈ antidiagonal e
a✝ : (u, snd✝) ≠ (e, 0)
⊢ u ≤ e

pp: case a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsRight R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff y) x = (coeff y) 0
u snd✝ : σ →₀ ℕ
huv : (u, snd✝) ∈ antidiagonal e
a✝ : (u, snd✝) ≠ (e, 0)
⊢ u ≠ e

Tactic:
· simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_right, zero_le]

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsRight R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff y) x = (coeff y) 0
u snd✝ : σ →₀ ℕ
huv : (u, snd✝) ∈ antidiagonal e
a✝ : (u, snd✝) ≠ (e, 0)
⊢ u ≠ e
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x✝ : ∃ i, {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U
ε : (ofClass v).ValueGroup₀ˣ
hε : {p | v.restrict (p.2 - p.1) < ↑ε} ⊆ U
δ : ℝ≥0 := (RankOne.hom v) ↑ε
hδ : δ = (RankOne.hom v) ↑ε
⊢ 0 < δ

Tactic:
rw [hδ, ← map_zero hv.hom]

Goal state after:
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x✝ : ∃ i, {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U
ε : (ofClass v).ValueGroup₀ˣ
hε : {p | v.restrict (p.2 - p.1) < ↑ε} ⊆ U
δ : ℝ≥0 := (RankOne.hom v) ↑ε
hδ : δ = (RankOne.hom v) ↑ε
⊢ (RankOne.hom v) 0 < (RankOne.hom v) ↑ε
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
⊢ {x | x ∈ v.integer} = Metric.closedBall 0 1

Tactic:
by
  ext x
  simp [mem_integer_iff]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h3 : 3 = 0
⊢ ofJ 0 = ofJ1728 F

Tactic:
rw [ofJ, if_pos rfl, if_pos h3]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
F : Cᵒᵖ ⥤ Type u_2
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
heq :
  (ConcreteCategory.hom ((E.toPreOneHypercover.multicospanIndex F).fst ⟨(i, j), PUnit.unit⟩))
      (s.val (E.toPreOneHypercover.multicospanShape.fst ⟨(i, j), PUnit.unit⟩)) =
    (ConcreteCategory.hom ((E.toPreOneHypercover.multicospanIndex F).snd ⟨(i, j), PUnit.unit⟩))
      (s.val (E.toPreOneHypercover.multicospanShape.snd ⟨(i, j), PUnit.unit⟩))
⊢ (ConcreteCategory.hom (F.map gi.op)) (s.val i) = (ConcreteCategory.hom (F.map gj.op)) (s.val j)

Tactic:
dsimp at heq

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
F : Cᵒᵖ ⥤ Type u_2
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
heq :
  (ConcreteCategory.hom (F.map (pullback.fst (E.f i) (E.f j)).op)) (s.val i) =
    (ConcreteCategory.hom (F.map (pullback.snd (E.f i) (E.f j)).op)) (s.val j)
⊢ (ConcreteCategory.hom (F.map gi.op)) (s.val i) = (ConcreteCategory.hom (F.map gj.op)) (s.val j)
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : GrothendieckTopology C
X : C
E : J.OneHypercover X
F : Cᵒᵖ ⥤ Type u_2
hF : Presieve.IsSheaf J F
R : Presieve X
h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) (Sieve.generate R)).arrows
h₂ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) (Sieve.generate R)).arrows
⊢ Presieve.IsSheafFor F R

Tactic:
rw [Presieve.isSheafFor_iff_generate]
  exact E.isSheafFor_sieve_of_pullback hF h₁ h₂

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
S : C
ι : Type u_3
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝⁴ : (ofArrows X f).HasPairwisePullbacks
c : Cofan X
hc : IsColimit c
hc' : IsUniversalColimit c
inst✝³ : HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)
inst✝² : ∀ (i : ι), HasPullback (f i) (Cofan.IsColimit.desc hc f)
F : Cᵒᵖ ⥤ Type u_4
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
inst✝ : PreservesLimit (Discrete.functor fun ij ↦ op (Limits.pullback (f ij.1) (f ij.2))) F
⊢ IsSheafFor F (singleton (Cofan.IsColimit.desc hc f)) ↔ IsSheafFor F (ofArrows X f)

Tactic:
let E := PreZeroHypercover.mk _ _ f

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
S : C
ι : Type u_3
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝⁴ : (ofArrows X f).HasPairwisePullbacks
c : Cofan X
hc : IsColimit c
hc' : IsUniversalColimit c
inst✝³ : HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)
inst✝² : ∀ (i : ι), HasPullback (f i) (Cofan.IsColimit.desc hc f)
F : Cᵒᵖ ⥤ Type u_4
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
inst✝ : PreservesLimit (Discrete.functor fun ij ↦ op (Limits.pullback (f ij.1) (f ij.2))) F
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
⊢ IsSheafFor F (singleton (Cofan.IsColimit.desc hc f)) ↔ IsSheafFor F (ofArrows X f)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Projective F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ⇑f ∘ P ≈ ⇑f ∘ Q
hz : ¬f (P z) = 0
⊢ P ≈ Q

Tactic:
· refine equiv_of_X_eq_of_Y_eq ((map_ne_zero_iff f f.injective).mp hz)
        ((map_ne_zero_iff f f.injective).mp <| hz.comp (Z_eq_zero_of_equiv h).mpr) ?_ ?_
      all_goals apply f.injective; map_simp
      exacts [X_eq_of_equiv h, Y_eq_of_equiv h]

Goal state after:
Module: Mathlib.RingTheory.Smooth.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
⊢ IsOpen (smoothLocus R A)

Tactic:
rw [isOpen_iff_forall_mem_open]
  intro x hx
  obtain ⟨_, ⟨_, ⟨f, rfl⟩, rfl⟩, hxf, hf⟩ :=
    isBasis_basic_opens.exists_subset_of_mem_open
    (smoothLocus_eq_compl_support_inter.le hx).2 Module.isOpen_freeLocus
  rw [Module.basicOpen_subset_freeLocus_iff] at hf
  let Af := Localization.Away f
  have : Algebra.FinitePresentation A (Localization.Away f) :=
    IsLocalization.Away.finitePresentation f
  have : Algebra.FinitePresentation R (Localization.Away f) :=
    .trans _ A _
  have : IsOpen (smoothLocus R Af) := by
    have := IsLocalizedModule.iso (.powers f)
      (KaehlerDifferential.map R R A (Localization.Away f))
    have := this.extendScalarsOfIsLocalization (.powers f) (Localization.Away f)
    have := Module.Projective.of_equiv this
    rw [smoothLocus_eq_compl_support_inter, Module.support_eq_zeroLocus]
    exact (isClosed_zeroLocus _).isOpen_compl.inter Module.isOpen_freeLocus
  rw [← smoothLocus_comap_of_isLocalization f] at this
  replace this := (PrimeSpectrum.localization_away_isOpenEmbedding Af f).isOpenMap _ this
  rw [Set.image_preimage_eq_inter_range, localization_away_comap_range Af f] at this
  exact ⟨_, Set.inter_subset_left, this, hx, hxf⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.dblX P * P z + 9 * (W'.a₁ * P x ^ 2 + 2 * P x * P y) * 0 -
      (((eval P) W'.polynomialX ^ 2 - W'.a₁ * (eval P) W'.polynomialX * P z * (P y - W'.negY P) -
              W'.a₂ * P z ^ 2 * (P y - W'.negY P) ^ 2 -
            2 * P x * P z * (P y - W'.negY P) ^ 2) *
          (P y - W'.negY P) +
        9 * (W'.a₁ * P x ^ 2 + 2 * P x * P y) *
          (P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3))) =
    0

Tactic:
(rw [dblX, eval_polynomialX, negY]; ring1)

Goal state after:
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
a : A
x✝ : S
y✝ : Ω[A⁄R]
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • x✝ ⊗ₜ[R] y✝) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) (x✝ ⊗ₜ[R] y✝)

pp: case tmul.add
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
a : A
x✝ y✝ : S ⊗[R] Ω[A⁄R]
a✝¹ :
  (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • x✝) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) x✝
a✝ :
  (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • y✝) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) y✝
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • (x✝ + y✝)) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) (x✝ + y✝)

Tactic:
· simp [smul_comm]

Goal state after:
case tmul.add
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
a : A
x✝ y✝ : S ⊗[R] Ω[A⁄R]
a✝¹ :
  (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • x✝) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) x✝
a✝ :
  (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • y✝) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) y✝
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • (x✝ + y✝)) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) (x✝ + y✝)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
x y : B
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B)))
      ((derivationTensorProduct R S A B).liftKaehlerDifferential ((D S B).tensorProductTo (x ⊗ₜ[S] y))) =
    (D S B).tensorProductTo (x ⊗ₜ[S] y)

Tactic:
simp only [Derivation.tensorProductTo_tmul, LinearMap.map_smul,
        Derivation.liftKaehlerDifferential_comp_D, map_liftBaseChange_smul]
      induction y using h.1.inductionOn
      · simp only [map_zero, smul_zero]
      · simp only [AlgHom.toLinearMap_apply, IsScalarTower.coe_toAlgHom',
          derivationTensorProduct_algebraMap, LinearMap.liftBaseChange_tmul,
          LinearMap.coe_restrictScalars, map_D, one_smul]
      · -- We use the specialized version of `map_smul` here for performance.
        simp only [Derivation.map_smul, LinearMap.map_smul, *, smul_comm x]
      · simp only [map_add, smul_add, *]

Goal state after:
Module: Mathlib.RingTheory.Smooth.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S := IsLocalization.liftAlgHom ⋯
s : P
hs : s ∈ M
x : MvPolynomial (Fin n) R
⊢ ∃ a, fP a = IsLocalization.mk' S (f₀ x) ⟨s, hs⟩

Tactic:
obtain ⟨s, rfl⟩ := hf₀ s

Goal state after:
R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S := IsLocalization.liftAlgHom ⋯
x s : MvPolynomial (Fin n) R
hs : f₀ s ∈ M
⊢ ∃ a, fP a = IsLocalization.mk' S (f₀ x) ⟨f₀ s, hs⟩
Module: Mathlib.RingTheory.Smooth.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Module.Flat R S
inst✝² : FinitePresentation R S
q : Ideal S
inst✝¹ : q.IsPrime
inst✝ : IsUnramifiedAt R q
⊢ IsEtaleAt R q

Tactic:
by
  obtain ⟨f, hfp, H⟩ := exists_unramified_of_isUnramifiedAt (R := R) q
  change ⟨q, ‹_›⟩ ∈ etaleLocus R S
  suffices Algebra.Etale R (Localization.Away f) from
    (basicOpen_subset_etaleLocus_iff (R := R) (f := f)).mpr inferInstance hfp
  exact .of_formallyUnramified_of_flat

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
x : AdicCompletion I (⨁ (j : ι), M j)
j : ι
⊢ (component (AdicCompletion I R) ι (fun i ↦ AdicCompletion I (M i)) j) ((sumInv I M) x) = (map I (component R ι M j)) x

Tactic:
apply induction_on I _ x (fun x ↦ ?_)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
x✝ : AdicCompletion I (⨁ (j : ι), M j)
j : ι
x : AdicCauchySequence I (⨁ (j : ι), M j)
⊢ (component (AdicCompletion I R) ι (fun i ↦ AdicCompletion I (M i)) j) ((sumInv I M) ((mk I (⨁ (j : ι), M j)) x)) =
    (map I (component R ι M j)) ((mk I (⨁ (j : ι), M j)) x)
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
x : AdicCompletion I (⨁ (j : ι), M j)
j : ι
⊢ ((sumInv I M) x) j = (map I (component R ι M j)) x

Tactic:
apply induction_on I _ x (fun x ↦ ?_)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Fintype ι
x✝ : AdicCompletion I (⨁ (j : ι), M j)
j : ι
x : AdicCauchySequence I (⨁ (j : ι), M j)
⊢ ((sumInv I M) ((mk I (⨁ (j : ι), M j)) x)) j = (map I (component R ι M j)) ((mk I (⨁ (j : ι), M j)) x)
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
K✝ : Type u_3
P✝ : Type u_4
inst✝¹³ : Ring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup K✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ K✝
inst✝⁷ : Module R✝ P✝
g✝ : M✝ →ₗ[R✝] P✝
s✝ : M✝ →ₗ[R✝] K✝
κ✝ : Type u_6
σ✝ : Type u_7
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
m : M
h : m ∈ s.ker
⊢ g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))

Tactic:
have : m ∈ Submodule.span R (Set.range v) := hsp Submodule.mem_top

Goal state after:
R✝ : Type u_1
M✝ : Type u_2
K✝ : Type u_3
P✝ : Type u_4
inst✝¹³ : Ring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup K✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ K✝
inst✝⁷ : Module R✝ P✝
g✝ : M✝ →ₗ[R✝] P✝
s✝ : M✝ →ₗ[R✝] K✝
κ✝ : Type u_6
σ✝ : Type u_7
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
κ : Type u_6
σ : Type u_7
v : κ ⊕ σ → M
hg : Function.Surjective ⇑g
hslzero : ∀ (i : κ), s (v (Sum.inl i)) = 0
hli : LinearIndependent R (⇑s ∘ v ∘ Sum.inr)
hsp : ⊤ ≤ Submodule.span R (Set.range v)
m : M
h : m ∈ s.ker
this : m ∈ Submodule.span R (Set.range v)
⊢ g m ∈ Submodule.span R (Set.range (⇑g ∘ v ∘ Sum.inl))