mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
⊢ ↑({x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} ∩
        ↑(ZLattice.comap ℝ (idealLattice K ((FractionalIdeal.mk0 K) J)) ↑↑(toMixed K))) ≃
    { a // mixedEmbedding.norm ↑a ≤ s }

Tactic:
rw [ZLattice.coe_comap]
  refine (((toMixed K).toEquiv.image _).trans (Equiv.subtypeEquivProp ?_)).trans
    (Equiv.subtypeSubtypeEquivSubtypeInter _ (mixedEmbedding.norm · ≤ s)).symm
  ext
  simp_rw [mem_idealSet, Set.mem_image, Set.mem_inter_iff, Set.mem_preimage, SetLike.mem_coe,
    mem_idealLattice, FractionalIdeal.coe_mk0]
  constructor
  · rintro ⟨_, ⟨⟨hx₁, hx₂⟩, _, ⟨x, hx₃, rfl⟩, h⟩, rfl⟩
    exact ⟨⟨hx₁, x, hx₃, h⟩, hx₂⟩
  · rintro ⟨⟨hx₁, ⟨x, hx₂, rfl⟩⟩, hx₃⟩
    exact ⟨(toMixed K).symm (mixedEmbedding K x), ⟨⟨hx₁, hx₃⟩, ⟨(x : K), by simp [hx₂], rfl⟩⟩, rfl⟩

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : v ∈ T
⊢ A *ᵥ v ∈ S

Tactic:
by
  rw [mem_Icc] at hv ⊢
  have mulVec_def : A.mulVec v =
      fun i ↦ Finset.sum univ fun j : β ↦ A i j * v j := rfl
  rw [mulVec_def]
  refine ⟨fun i ↦ ?_, fun i ↦ ?_⟩
  all_goals
    simp only [mul_neg]
    gcongr ∑ _ : β, ?_ with j _ -- Get rid of sums
    rw [← mul_comm (v j)] -- Move A i j to the right of the products
    -- We have to distinguish cases: we have now 4 goals
    rcases le_total 0 (A i j) with hsign | hsign
  · rw [negPart_eq_zero.2 hsign]
    exact mul_nonneg (hv.1 j) hsign
  · rw [negPart_eq_neg.2 hsign]
    simp only [mul_neg, neg_neg]
    exact mul_le_mul_of_nonpos_right (hv.2 j) hsign
  · rw [posPart_eq_self.2 hsign]
    gcongr
    apply hv.2
  · rw [posPart_eq_zero.2 hsign]
    exact mul_nonpos_of_nonneg_of_nonpos (hv.1 j) hsign

Goal state after:
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
u : K →+* ℂ
| (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u

Tactic:
sum_mul

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
u : K →+* ℂ
| ∑ i, (∑ l, ↑(a' K a k l i u) * ↑(x (l, i))) * (newBasis K) u
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
i : α
⊢ ↑(#(Icc (∑ j, ↑B * -(A i j)⁻) (∑ j, ↑B * (A i j)⁺))) = P i - N i + 1

Tactic:
Int.card_Icc_of_le (N i) (P i) (N_le_P_add_one A i)

Goal state after:
case e_f
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
i : α
⊢ P i + 1 - N i = P i - N i + 1
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1
r l : K →+* ℂ
| (∑ l_1, ↑(a' K a k l_1 r l) * ↑(x (l_1, r))) * (newBasis K) l

Tactic:
sum_mul

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1
r l : K →+* ℂ
| ∑ i, ↑(a' K a k i r l) * ↑(x (i, r)) * (newBasis K) l
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
⊢ ‖asiegel K a‖ ≤ c₂ K * A

Tactic:
by
  have := c_nonneg K
  rw [Matrix.norm_le_iff]
  · intro kr lu
    calc
      ‖asiegel K a kr lu‖ = |asiegel K a kr lu| := ?_
      _ ≤ c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1 * ((newBasis K) lu.2))) := ?_
      _ ≤ c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) *
        house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) := ?_
      _ ≤ c K * A * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) := ?_
      _ ≤ c K * A * supOfBasis K := ?_
      _ ≤ c₂ K * A := ?_
    · simp only [Int.cast_abs, ← Real.norm_eq_abs (asiegel K a kr lu)]; rfl
    · have remark := basis_repr_norm_le_const_mul_house K
      simp only [Basis.repr_reindex, Finsupp.mapDomain_equiv_apply,
        integralBasis_repr_apply, eq_intCast, Rat.cast_intCast,
          Complex.norm_intCast] at remark
      exact mod_cast remark ((a kr.1 lu.1 * ((newBasis K) lu.2))) kr.2
    · simp only [house, map_mul, mul_assoc]
      gcongr
      apply norm_mul_le
    · rw [mul_assoc, mul_assoc]
      gcongr _ * (?_ * _)
      · apply house_nonneg
      · exact habs kr.1 lu.1
    · gcongr
      simp only [supOfBasis, le_sup'_iff, mem_univ]; use lu.2
    · rw [mul_right_comm, c₂]
      gcongr
      exacts [supOfBasis_nonneg _, le_max_right ..]
  · exact mul_nonneg (c₂_nonneg _) Apos

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : MetricSpace Y
inst✝ : IsUltrametricDist Y
f g h : C(X, Y)
⊢ dist f h ≤ max (dist f g) (dist g h)

Tactic:
ContinuousMap.dist_le (by positivity)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : MetricSpace Y
inst✝ : IsUltrametricDist Y
f g h : C(X, Y)
⊢ ∀ (x : X), dist (f x) (h x) ≤ max (dist f g) (dist g h)
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
s t : ℝ
hfm : f ↑m = ↑m ^ s
hfn : f ↑n = ↑n ^ t
⊢ f ↑m ^ logb ↑m ↑n ≤ ↑n ^ s

Tactic:
hfm,

Goal state after:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
s t : ℝ
hfm : f ↑m = ↑m ^ s
hfn : f ↑n = ↑n ^ t
⊢ (↑m ^ s) ^ logb ↑m ↑n ≤ ↑n ^ s
Module: Mathlib.NumberTheory.Padics.Complex

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ (fun x ↦ ‖x‖) = Norm.norm

Tactic:
by
  with_reducible_and_instances rfl

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
x : X
hx : x ∈ univ
j : Fin n
hj : x ∈ ↑(W j)
⊢ W j ≠ ⊥

Tactic:
simpa [← SetLike.coe_ne_coe, ← Set.nonempty_iff_ne_empty] using ⟨x, hj⟩

Goal state after:
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (Rat.padicValuation p).Completion
⊢ ‖withValUniformEquiv x‖ ≤ 1 ↔ Valued.v x ≤ 1

Tactic:
induction x using UniformSpace.Completion.induction_on with
  | hp =>
    rw [Set.ext fun _ ↦ Iff.comm]
    simp_rw [← Valuation.restrict_le_one_iff Valued.v]
    apply withValUniformEquiv.toHomeomorph.isClosed_setOfPred_iff (q := fun x ↦ ‖x‖ ≤ 1)
      (Valued.isClopen_closedBall _ one_ne_zero)
    simpa [Metric.closedBall] using IsUltrametricDist.isClopen_closedBall (0 : ℚ_[p]) one_ne_zero
  | ih a =>
    rw [Valued.valuedCompletion_apply, ← WithVal.apply_ofVal, withValUniformEquiv_cast_apply]
    exact (norm_rat_le_one_iff_padicValuation_le_one p)

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: case refine_4
ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
⊢ Pairwise (Disjoint on fun k ↦ W ↑(t.equivFin.symm k))

Tactic:
exact hWd.comp_of_injective <| Subtype.val_injective.comp t.equivFin.symm.injective

Goal state after:
Module: Mathlib.NumberTheory.PrimesCongruentOne

Goal state before:
pp: case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]

Tactic:
refine ⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩

Goal state after:
case inr.refine_1
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
habs : p ≤ n
⊢ False

case inr.refine_2
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
⊢ p ≡ 1 [MOD k]
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
H : a.y = 0
prop : a.x = 1 ∨ a.x = -1
⊢ a = 1 ∨ a = -1

Tactic:
exact prop.imp (fun h => ext h H) fun h => ext h H

Goal state after:
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
ha : (Polynomial.aeval a) F = 0
z' : ℤ_[p]
hz' : (Polynomial.aeval z') F = 0
hnormz' : ‖z' - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  (Polynomial.aeval (a + h)) F = (Polynomial.aeval a) F + (Polynomial.aeval a) (Polynomial.derivative F) * h + q * h ^ 2
⊢ ((Polynomial.aeval a) (Polynomial.derivative F) + q * h) * h = (Polynomial.aeval (a + h)) F

Tactic:
hq,

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
ha : (Polynomial.aeval a) F = 0
z' : ℤ_[p]
hz' : (Polynomial.aeval z') F = 0
hnormz' : ‖z' - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  (Polynomial.aeval (a + h)) F = (Polynomial.aeval a) F + (Polynomial.aeval a) (Polynomial.derivative F) * h + q * h ^ 2
⊢ ((Polynomial.aeval a) (Polynomial.derivative F) + q * h) * h =
    (Polynomial.aeval a) F + (Polynomial.aeval a) (Polynomial.derivative F) * h + q * h ^ 2
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = 0}.Infinite
q : ℚ
hq : q.num ^ 2 - d * ↑q.den ^ 2 = 0
⊢ False

Tactic:
sub_eq_zero,

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = 0}.Infinite
q : ℚ
hq : q.num ^ 2 = d * ↑q.den ^ 2
⊢ False
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
⊢ ↑⋯.unit = ↑(LinearOrderedCommGroup.Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup)

Tactic:
Units.val_inj

Goal state after:
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
⊢ ⋯.unit = LinearOrderedCommGroup.Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case neg
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
⊢ ∑ i ∈ n.divisors, (∑ d ∈ n.divisors, weights d) * weights i =
    ∑ y ∈ n.divisors, ∑ x ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = y.lcm d2 then weights y * weights d2 else 0

Tactic:
sum_mul

Goal state after:
case neg
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
⊢ ∑ x ∈ n.divisors, ∑ i ∈ n.divisors, weights i * weights x =
    ∑ y ∈ n.divisors, ∑ x ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = y.lcm d2 then weights y * weights d2 else 0
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case h
R : Type u
inst✝¹⁵ : CommRing R
S : Type v
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker f ≠ ⊤
F : V'' →ₗ[R] V
hf : Function.Injective ⇑F
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : ∑ i ∈ s, g i • (⇑F ∘ b) i = 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI✝ : a * g j ∉ ↑(RingHom.ker f)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : ι → R := fun i ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K) (g' i) = a * g i
hgI : f (g' j) ≠ 0
⊢ ∑ i ∈ s, (fun i ↦ f (g' i)) i • (⇑f' ∘ b) i = 0

Tactic:
have eq : F (∑ i ∈ s, g' i • b i) = 0 := by
    rw [map_sum, ← smul_zero a, ← eq, Finset.smul_sum]
    refine Finset.sum_congr rfl ?_
    intro i hi
    rw [map_smul, ← IsScalarTower.algebraMap_smul K, hg' i hi, ← smul_assoc,
      smul_eq_mul, Function.comp_apply]

Goal state after:
case h
R : Type u
inst✝¹⁵ : CommRing R
S : Type v
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker f ≠ ⊤
F : V'' →ₗ[R] V
hf : Function.Injective ⇑F
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq✝ : ∑ i ∈ s, g i • (⇑F ∘ b) i = 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI✝ : a * g j ∉ ↑(RingHom.ker f)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : ι → R := fun i ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K) (g' i) = a * g i
hgI : f (g' j) ≠ 0
eq : F (∑ i ∈ s, g' i • b i) = 0
⊢ ∑ i ∈ s, (fun i ↦ f (g' i)) i • (⇑f' ∘ b) i = 0
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b x y u v : R
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ a * b = (x * u - y * v) ^ 2 + (x * v + y * u) ^ 2

Tactic:
by rw [ha, hb]; ring

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case neg
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
h : |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ≤ c
hx : x ∈ Set.Ioc 0 1
hx1 : 1 < x * ‖s‖
⊢ (x * ‖s‖) ^ (p - 1) ≤ (x * ‖s‖) ^ p

Tactic:
exact pow_le_pow_right₀ hx1.le (Nat.sub_le _ _)

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case pos
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Tactic:
have := (finiteDimensional_iff_of_rank_eq_nsmul he hdim).mpr hP

Goal state after:
case pos
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
this : FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
m : ℤ
⊢ LiouvilleWith p (x - ↑m) ↔ LiouvilleWith p x

Tactic:
by
  rw [← Rat.cast_intCast, sub_rat_iff]

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
c : Concept α β r
⊢ c ≤ ofAttributes r t ↔ t ⊆ c.intent

Tactic:
by
  rw [← intent_subset_intent_iff]
  exact ⟨((subset_upperPolar_lowerPolar r t).trans ·),
    (isIntent_intent c).upperPolar_lowerPolar_subset⟩

Goal state after:
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
⊢ False

Tactic:
hs.eq_of_le (y := s') ?_ fun _ _ ↦ Or.inl

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
h : ¬s' x y ∧ ¬s' y x
⊢ False

α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
⊢ s' ∈ S
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
⊢ IsStronglyAtomic αs

Tactic:
simp_rw [isStronglyAtomic_iff, lt_iff_le_and_ne, hcovby]

Goal state after:
α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
⊢ ∀ (a b : αs), a ≤ b ∧ a ≠ b → ∃ x, (a ≤ x ∧ a.fst + 1 = x.fst) ∧ x ≤ b
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : CompleteLattice X
x✝ : Set (Nucleus X)
⊢ sInf x✝ ∈ lowerBounds x✝

Tactic:
by simp +contextual [mem_lowerBounds, ← coe_le_coe, Pi.le_def, iInf_le_iff]

Goal state after:
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
⊢ R.leftDual J ∈ R.rightFixedPoints

Tactic:
apply le_antisymm
  · apply R.gc_leftDual_rightDual.monotone_l; exact R.gc_leftDual_rightDual.le_u_l J
  · exact R.gc_leftDual_rightDual.l_u_le (R.leftDual J)

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
a : α
ha : a ∈ removeBot {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} ⋯ ⋯
⊢ ∃ y ∈ Q, a ≤ y

Tactic:
obtain ⟨⟨p, hp, q, hq, rfl⟩, h⟩ := ha
    grind [inf_le_right]

Goal state after:
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: o : OrderType.{u_1}
⊢ type o.ToType = 0 ↔ o = 0

Tactic:
type_toType

Goal state after:
o : OrderType.{u_1}
⊢ o = 0 ↔ o = 0
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: o : OrderType.{u_1}
⊢ type o.ToType ≠ 0 ↔ o ≠ 0

Tactic:
type_toType

Goal state after:
o : OrderType.{u_1}
⊢ o ≠ 0 ↔ o ≠ 0
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a b : X
⊢ sInf {s | a ⊓ b ≤ ↑s} = sInf {s | a ≤ ↑s} ⊓ sInf {s | b ≤ ↑s}

Tactic:
change Sublocale.restrictAux S (a ⊓ b) = Sublocale.restrictAux S a ⊓ Sublocale.restrictAux S b

Goal state after:
X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a b : X
⊢ Sublocale.restrictAux✝ S (a ⊓ b) = Sublocale.restrictAux✝ S a ⊓ Sublocale.restrictAux✝ S b
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
c : ℝ
n : ℕ
⊢ martingalePart (c • f) ℱ μ n =ᵐ[μ] c • martingalePart f ℱ μ n

Tactic:
by
  filter_upwards [predictablePart_smul (f := f) c n] with ω hω
  simpa [martingalePart, smul_sub]

Goal state after: