harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/FLT/Three.lean
/-- If `p : 𝓞 K` is a prime that divides both `S.a + S.b` and `S.a + η * S.b`, then `p`
is associated with `λ`. -/
lemma associated_of_dvd_a_add_b_of_dvd_a_add_eta_mul_b {p : 𝓞 K} (hp : Prime p)
    (hpab : p ∣ S.a + S.b) (hpaηb : p ∣ S.a + η * S.b) : Associated p λ

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ S.a + S.b
hpaηb : p ∣ S.a + ↑η * S.b
⊢ Associated p λ

Tactic:
suffices p_lam : p ∣ λ from hp.associated_of_dvd hζ.zeta_sub_one_prime' p_lam

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ S.a + S.b
hpaηb : p ∣ S.a + ↑η * S.b
⊢ p ∣ λ

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ 1 * S.a + 1 * S.b
hpaηb : p ∣ S.a + ↑η * S.b
⊢ p ∣ λ

Tactic:
rw [← one_mul S.a] at hpaηb

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ 1 * S.a + 1 * S.b
hpaηb : p ∣ 1 * S.a + ↑η * S.b
⊢ p ∣ λ

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ 1 * S.a + 1 * S.b
hpaηb : p ∣ 1 * S.a + ↑η * S.b
this : p ∣ (1 * ↑η - 1 * 1) * gcd S.a S.b
⊢ p ∣ λ

Tactic:
rwa [one_mul, one_mul, coe_eta, IsUnit.dvd_mul_right <| (gcd_isUnit_iff _ _).2 S.coprime] at this

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ S.a + S.b
hpaηb : p ∣ S.a + ↑η * S.b
⊢ p ∣ λ

Tactic:
rw [← one_mul S.a, ← one_mul S.b] at hpab

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ 1 * S.a + 1 * S.b
hpaηb : p ∣ S.a + ↑η * S.b
⊢ p ∣ λ

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ 1 * S.a + 1 * S.b
hpaηb : p ∣ 1 * S.a + ↑η * S.b
⊢ p ∣ λ

Tactic:
have := dvd_mul_sub_mul_mul_gcd_of_dvd hpab hpaηb

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ 1 * S.a + 1 * S.b
hpaηb : p ∣ 1 * S.a + ↑η * S.b
this : p ∣ (1 * ↑η - 1 * 1) * gcd S.a S.b
⊢ p ∣ λ
-- Mathlib/RingTheory/RingHom/StandardSmooth.lean
lemma isStandardSmoothOfRelativeDimension_respectsIso :
    RespectsIso (@IsStandardSmoothOfRelativeDimension.{t, w} n) where
  left {R S T _ _ _} f e hf

Proof state:
n : ℕ
R S T : Type u_2
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension (n + 0) (f.comp e.toRingHom)

Tactic:
exact hf.comp (IsStandardSmoothOfRelativeDimension.equiv e)

Result:
no goals

Proof state:
n : ℕ
R S T : Type u_2
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension n (f.comp e.toRingHom)

Tactic:
rw [← add_zero n]

Result:
n : ℕ
R S T : Type u_2
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension (n + 0) (f.comp e.toRingHom)

Proof state:
n : ℕ
R S T : Type u_2
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension (0 + n) (e.toRingHom.comp f)

Tactic:
exact (IsStandardSmoothOfRelativeDimension.equiv e).comp hf

Result:
no goals

Proof state:
n : ℕ
R S T : Type u_2
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension n (e.toRingHom.comp f)

Tactic:
rw [← zero_add n]

Result:
n : ℕ
R S T : Type u_2
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension (0 + n) (e.toRingHom.comp f)
-- Mathlib/Computability/Reduce.lean
theorem ManyOneReducible.trans {α β γ} [Primcodable α] [Primcodable β] [Primcodable γ]
    {p : α → Prop} {q : β → Prop} {r : γ → Prop} : p ≤₀ q → q ≤₀ r → p ≤₀ r
  | ⟨f, c₁, h₁⟩, ⟨g, c₂, h₂⟩ =>
    ⟨g ∘ f, c₂.comp c₁,
      fun a => ⟨fun h => by erw [← h₂, ← h₁]; assumption, fun h => by rwa [h₁, h₂]⟩⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : p a
⊢ r ((g ∘ f) a)

Tactic:
erw [← h₂, ← h₁]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : p a
⊢ p a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : r ((g ∘ f) a)
⊢ p a

Tactic:
rwa [h₁, h₂]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → β
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : p a
⊢ p a

Tactic:
assumption

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem NFBelow.fst {e n a b} (h : NFBelow (ONote.oadd e n a) b) : NF e

Proof state:
case oadd'
e : ONote
n : ℕ+
a : ONote
b eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
⊢ e.NF

Tactic:
exact ⟨⟨_, h₁⟩⟩

Result:
no goals

Proof state:
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
h : (e.oadd n a).NFBelow b
⊢ e.NF

Tactic:
obtain - | ⟨h₁, h₂, h₃⟩ := h

Result:
case oadd'
e : ONote
n : ℕ+
a : ONote
b eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
⊢ e.NF
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem IsSuffix.getLast {x y : List α} (h : x <:+ y) (hx : x ≠ []) :
    x.getLast hx = y.getLast (h.ne_nil hx)

Proof state:
α : Type u_1
x y : List α
h✝ : x <:+ y
hx : x ≠ []
h : y.reverse = []
⊢ False

Tactic:
simp only [reverse_eq_nil_iff] at h

Result:
α : Type u_1
x y : List α
h✝ : x <:+ y
hx : x ≠ []
h : y = []
⊢ False

Proof state:
α : Type u_1
x y : List α
h✝ : x <:+ y
hx : x ≠ []
h : y = []
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
x y : List α
h : x <:+ y
hx : x ≠ []
⊢ x.getLast hx = y.getLast ⋯

Tactic:
rw [← head_reverse (by simpa), h.reverse.head,
  head_reverse (by rintro h; simp only [reverse_eq_nil_iff] at h; simp_all)]

Result:
no goals

Proof state:
α : Type u_1
x y : List α
h : x <:+ y
hx : x ≠ []
⊢ y.reverse ≠ []

Tactic:
rintro h

Result:
α : Type u_1
x y : List α
h✝ : x <:+ y
hx : x ≠ []
h : y.reverse = []
⊢ False

Proof state:
α : Type u_1
x y : List α
h : x <:+ y
hx : x ≠ []
⊢ x.reverse ≠ []

Tactic:
simpa

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem iff_isSplitEpi_eq_zero {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] : IsZero Y ↔ f = 0

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
h : f = 0
⊢ 𝟙 Y = 0

Tactic:
rw [← IsSplitEpi.id f]

Result:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
h : f = 0
⊢ section_ f ≫ f = 0

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
h : f = 0
⊢ section_ f ≫ f = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ 𝟙 Y = 0 ↔ f = 0

Tactic:
constructor

Result:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ 𝟙 Y = 0 → f = 0

case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ f = 0 → 𝟙 Y = 0

Proof state:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
h : 𝟙 Y = 0
⊢ f = 0

Tactic:
rw [← Category.comp_id f, h, comp_zero]

Result:
no goals

Proof state:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ 𝟙 Y = 0 → f = 0

Tactic:
intro h

Result:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
h : 𝟙 Y = 0
⊢ f = 0

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ f = 0 → 𝟙 Y = 0

Tactic:
intro h

Result:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
h : f = 0
⊢ 𝟙 Y = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ IsZero Y ↔ f = 0

Tactic:
rw [iff_id_eq_zero]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ 𝟙 Y = 0 ↔ f = 0
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem le_minDegree_of_forall_le_degree [DecidableRel G.Adj] [Nonempty V] (k : ℕ)
    (h : ∀ v, k ≤ G.degree v) : k ≤ G.minDegree

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
k : ℕ
h : ∀ (v : V), k ≤ G.degree v
v : V
hv : G.minDegree = G.degree v
⊢ k ≤ G.degree v

Tactic:
apply h

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
k : ℕ
h : ∀ (v : V), k ≤ G.degree v
⊢ k ≤ G.minDegree

Tactic:
rcases G.exists_minimal_degree_vertex with ⟨v, hv⟩

Result:
case intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
k : ℕ
h : ∀ (v : V), k ≤ G.degree v
v : V
hv : G.minDegree = G.degree v
⊢ k ≤ G.minDegree

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
k : ℕ
h : ∀ (v : V), k ≤ G.degree v
v : V
hv : G.minDegree = G.degree v
⊢ k ≤ G.minDegree

Tactic:
rw [hv]

Result:
case intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
k : ℕ
h : ∀ (v : V), k ≤ G.degree v
v : V
hv : G.minDegree = G.degree v
⊢ k ≤ G.degree v
-- Mathlib/Probability/Distributions/Uniform.lean
theorem toMeasurable {X : Ω → E} {s : Set E} (hu : IsUniform X s ℙ μ) :
    IsUniform X (toMeasurable μ s) ℙ μ

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
⊢ IsUniform X (toMeasurable μ s) ℙ μ

Tactic:
unfold IsUniform at *

Result:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : Measure.map X ℙ = ProbabilityTheory.cond μ s
⊢ Measure.map X ℙ = ProbabilityTheory.cond μ (toMeasurable μ s)

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : Measure.map X ℙ = ProbabilityTheory.cond μ s
⊢ Measure.map X ℙ = ProbabilityTheory.cond μ (toMeasurable μ s)

Tactic:
rwa [ProbabilityTheory.cond_toMeasurable_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/RelabelFin.lean
theorem Clause.of_maxLiteral_eq_none (c : Clause Nat) (h : c.maxLiteral = none) :
    ∀ lit, ¬Mem lit c

Proof state:
c : Clause Nat
h : c.maxLiteral = none
lit : Nat
hlit : Mem lit c
⊢ False

Tactic:
simp only [maxLiteral, List.max?_eq_none_iff, List.map_eq_nil_iff] at h

Result:
c : Clause Nat
lit : Nat
hlit : Mem lit c
h : c = []
⊢ False

Proof state:
c : Clause Nat
h : c.maxLiteral = none
⊢ ∀ (lit : Nat), ¬Mem lit c

Tactic:
intro lit hlit

Result:
c : Clause Nat
h : c.maxLiteral = none
lit : Nat
hlit : Mem lit c
⊢ False

Proof state:
c : Clause Nat
lit : Nat
hlit : Mem lit c
h : c = []
⊢ False

Tactic:
simp only [h, not_mem_nil] at hlit

Result:
no goals
-- Mathlib/Data/List/OfFn.lean
theorem ofFn_add {m n} (f : Fin (m + n) → α) :
    List.ofFn f =
      (List.ofFn fun i => f (Fin.castAdd n i)) ++ List.ofFn fun j => f (Fin.natAdd m j)

Proof state:
α : Type u
m n : ℕ
f : Fin (m + n) → α
⊢ ofFn f = (ofFn fun i => f (Fin.castAdd n i)) ++ ofFn fun j => f (Fin.natAdd m j)

Tactic:
induction' n with n IH

Result:
case zero
α : Type u
m : ℕ
f : Fin (m + 0) → α
⊢ ofFn f = (ofFn fun i => f (Fin.castAdd 0 i)) ++ ofFn fun j => f (Fin.natAdd m j)

case succ
α : Type u
m n : ℕ
IH : ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (Fin.castAdd n i)) ++ ofFn fun j => f (Fin.natAdd m j)
f : Fin (m + (n + 1)) → α
⊢ ofFn f = (ofFn fun i => f (Fin.castAdd (n + 1) i)) ++ ofFn fun j => f (Fin.natAdd m j)

Proof state:
case zero
α : Type u
m : ℕ
f : Fin (m + 0) → α
⊢ ofFn f = (ofFn fun i => f (Fin.castAdd 0 i)) ++ ofFn fun j => f (Fin.natAdd m j)

Tactic:
rw [ofFn_zero, append_nil, Fin.castAdd_zero, Fin.cast_refl]

Result:
case zero
α : Type u
m : ℕ
f : Fin (m + 0) → α
⊢ ofFn f = ofFn fun i => f (id i)

Proof state:
case zero
α : Type u
m : ℕ
f : Fin (m + 0) → α
⊢ ofFn f = ofFn fun i => f (id i)

Tactic:
rfl

Result:
no goals

Proof state:
case succ
α : Type u
m n : ℕ
IH : ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (Fin.castAdd n i)) ++ ofFn fun j => f (Fin.natAdd m j)
f : Fin (m + (n + 1)) → α
⊢ ((ofFn fun i => f (Fin.castAdd n i).castSucc) ++ ofFn fun j => f (Fin.natAdd m j).castSucc).concat
      (f (Fin.last (m.add n))) =
    ((ofFn fun i => f (Fin.castAdd (n + 1) i)) ++ ofFn fun i => f (Fin.natAdd m i.castSucc)).concat
      (f (Fin.natAdd m (Fin.last n)))

Tactic:
rfl

Result:
no goals

Proof state:
case succ
α : Type u
m n : ℕ
IH : ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (Fin.castAdd n i)) ++ ofFn fun j => f (Fin.natAdd m j)
f : Fin (m + (n + 1)) → α
⊢ ofFn f = (ofFn fun i => f (Fin.castAdd (n + 1) i)) ++ ofFn fun j => f (Fin.natAdd m j)

Tactic:
rw [ofFn_succ', ofFn_succ', IH, append_concat]

Result:
case succ
α : Type u
m n : ℕ
IH : ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (Fin.castAdd n i)) ++ ofFn fun j => f (Fin.natAdd m j)
f : Fin (m + (n + 1)) → α
⊢ ((ofFn fun i => f (Fin.castAdd n i).castSucc) ++ ofFn fun j => f (Fin.natAdd m j).castSucc).concat
      (f (Fin.last (m.add n))) =
    ((ofFn fun i => f (Fin.castAdd (n + 1) i)) ++ ofFn fun i => f (Fin.natAdd m i.castSucc)).concat
      (f (Fin.natAdd m (Fin.last n)))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem and_zero (x : Nat) : x &&& 0 = 0

Proof state:
x : Nat
⊢ (if x = 0 then if (false && true) = true then 0 else 0
    else
      if 0 = 0 then if (true && false) = true then x else 0
      else
        let n' := x / 2;
        let m' := 0 / 2;
        let b₁ := x % 2 = 1;
        let b₂ := 0 % 2 = 1;
        let r := bitwise and n' m';
        if (decide b₁ && decide b₂) = true then r + r + 1 else r + r) =
    0

Tactic:
simp

Result:
no goals

Proof state:
x : Nat
⊢ bitwise and x 0 = 0

Tactic:
unfold bitwise

Result:
x : Nat
⊢ (if x = 0 then if (false && true) = true then 0 else 0
    else
      if 0 = 0 then if (true && false) = true then x else 0
      else
        let n' := x / 2;
        let m' := 0 / 2;
        let b₁ := x % 2 = 1;
        let b₂ := 0 % 2 = 1;
        let r := bitwise and n' m';
        if (decide b₁ && decide b₂) = true then r + r + 1 else r + r) =
    0

Proof state:
x : Nat
⊢ x &&& 0 = 0

Tactic:
simp only [HAnd.hAnd, AndOp.and, land]

Result:
x : Nat
⊢ bitwise and x 0 = 0
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive (attr := simp) toReal_enorm]
lemma toReal_enorm' (x : E) : ‖x‖ₑ.toReal = ‖x‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x : E
⊢ ‖x‖ₑ.toReal = ‖x‖

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/Data/Nat/Totient.lean
theorem sum_totient' (n : ℕ) : ∑ m ∈ range n.succ with m ∣ n, φ m = n

Proof state:
n : ℕ
⊢ ∑ m ∈ filter (fun m => m ∣ n) (range n.succ), φ m = n

Tactic:
convert sum_totient _ using 1

Result:
case h.e'_2
n : ℕ
⊢ ∑ m ∈ filter (fun m => m ∣ n) (range n.succ), φ m = n.divisors.sum φ

Proof state:
case h.e'_2
n : ℕ
⊢ (∑ a ∈ Ico 0 n.succ, if a ∣ n then φ a else 0) = ∑ a ∈ Ico 1 (n + 1), if a ∣ n then φ a else 0

Tactic:
rw [sum_eq_sum_Ico_succ_bot] <;> simp

Result:
no goals

Proof state:
case h.e'_2
n : ℕ
⊢ ∑ m ∈ filter (fun m => m ∣ n) (range n.succ), φ m = n.divisors.sum φ

Tactic:
simp only [Nat.divisors, sum_filter, range_eq_Ico]

Result:
case h.e'_2
n : ℕ
⊢ (∑ a ∈ Ico 0 n.succ, if a ∣ n then φ a else 0) = ∑ a ∈ Ico 1 (n + 1), if a ∣ n then φ a else 0
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem le_bmex_of_forall {o : Ordinal} (f : ∀ a < o, Ordinal) {a : Ordinal}
    (H : ∀ b < a, ∃ i hi, f i hi = b) : a ≤ bmex o f

Proof state:
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}
a : Ordinal.{max u_4 u_5}
H : ∀ b < a, ∃ i, ∃ (hi : i < o), f i hi = b
⊢ a ≤ o.bmex f

Tactic:
by_contra! h

Result:
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}
a : Ordinal.{max u_4 u_5}
H : ∀ b < a, ∃ i, ∃ (hi : i < o), f i hi = b
h : o.bmex f < a
⊢ False

Proof state:
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}
a : Ordinal.{max u_4 u_5}
H : ∀ b < a, ∃ i, ∃ (hi : i < o), f i hi = b
h : o.bmex f < a
⊢ False

Tactic:
exact bmex_not_mem_brange f (H _ h)

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
/-- See also `Order.succ_eq_of_covBy`. -/
lemma le_succ_of_wcovBy (h : a ⩿ b) : b ≤ succ a

Proof state:
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
hba : ¬b ≤ succ a
⊢ False

Tactic:
exact h.2 (lt_succ_of_not_isMax hab.lt.not_isMax) <| hab.lt.succ_le.lt_of_not_le hba

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
⊢ b ≤ succ a

Tactic:
obtain hab | ⟨-, hba⟩ := h.covBy_or_le_and_le

Result:
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
⊢ b ≤ succ a

case inr.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
hba : b ≤ a
⊢ b ≤ succ a

Proof state:
case inr.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
hba : b ≤ a
⊢ b ≤ succ a

Tactic:
exact hba.trans (le_succ _)

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
⊢ b ≤ succ a

Tactic:
by_contra hba

Result:
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
hba : ¬b ≤ succ a
⊢ False
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem denumerable_iff {α : Type u} : Nonempty (Denumerable α) ↔ #α = ℵ₀ :=
  ⟨fun ⟨h⟩ => mk_congr ((@Denumerable.eqv α h).trans Equiv.ulift.symm), fun h => by
    obtain ⟨f⟩ := Quotient.exact h
    exact ⟨Denumerable.mk' <| f.trans Equiv.ulift⟩⟩

Proof state:
α : Type u
h : #α = ℵ₀
⊢ Nonempty (Denumerable α)

Tactic:
obtain ⟨f⟩ := Quotient.exact h

Result:
case intro
α : Type u
h : #α = ℵ₀
f : α ≃ ULift.{u, 0} ℕ
⊢ Nonempty (Denumerable α)

Proof state:
case intro
α : Type u
h : #α = ℵ₀
f : α ≃ ULift.{u, 0} ℕ
⊢ Nonempty (Denumerable α)

Tactic:
exact ⟨Denumerable.mk' <| f.trans Equiv.ulift⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_rotateLeft {r n w : Nat} {x : BitVec w} :
    (x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w))

Proof state:
case neg
r n w : Nat
x : BitVec (w + 1)
h : ¬r < w
⊢ (decide (n < w + 1) && x.getMsbD ((r % (w + 1) + n) % (w + 1))) =
    (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

Tactic:
simp

Result:
no goals

Proof state:
case succ
r n w : Nat
x : BitVec (w + 1)
⊢ (x.rotateLeft r).getMsbD n = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

Tactic:
by_cases h : r < w

Result:
case pos
r n w : Nat
x : BitVec (w + 1)
h : r < w
⊢ (x.rotateLeft r).getMsbD n = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

case neg
r n w : Nat
x : BitVec (w + 1)
h : ¬r < w
⊢ (x.rotateLeft r).getMsbD n = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

Proof state:
case neg
r n w : Nat
x : BitVec (w + 1)
h : ¬r < w
⊢ (x.rotateLeft r).getMsbD n = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

Tactic:
rw [← rotateLeft_mod_eq_rotateLeft, getMsbD_rotateLeft_of_lt (by apply Nat.mod_lt; simp)]

Result:
case neg
r n w : Nat
x : BitVec (w + 1)
h : ¬r < w
⊢ (decide (n < w + 1) && x.getMsbD ((r % (w + 1) + n) % (w + 1))) =
    (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

Proof state:
r n w : Nat
x : BitVec (w + 1)
h : r < w
⊢ r < w + 1

Tactic:
omega

Result:
no goals

Proof state:
r n w : Nat
x : BitVec w
⊢ (x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w))

Tactic:
rcases w with rfl | w

Result:
case zero
r n : Nat
x : BitVec 0
⊢ (x.rotateLeft r).getMsbD n = (decide (n < 0) && x.getMsbD ((r + n) % 0))

case succ
r n w : Nat
x : BitVec (w + 1)
⊢ (x.rotateLeft r).getMsbD n = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

Proof state:
case pos
r n w : Nat
x : BitVec (w + 1)
h : r < w
⊢ (x.rotateLeft r).getMsbD n = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

Tactic:
rw [getMsbD_rotateLeft_of_lt (by omega)]

Result:
no goals

Proof state:
case a
r n w : Nat
x : BitVec (w + 1)
h : ¬r < w
⊢ w + 1 > 0

Tactic:
simp

Result:
no goals

Proof state:
case zero
r n : Nat
x : BitVec 0
⊢ (x.rotateLeft r).getMsbD n = (decide (n < 0) && x.getMsbD ((r + n) % 0))

Tactic:
simp

Result:
no goals

Proof state:
r n w : Nat
x : BitVec (w + 1)
h : ¬r < w
⊢ r % (w + 1) < w + 1

Tactic:
apply Nat.mod_lt

Result:
case a
r n w : Nat
x : BitVec (w + 1)
h : ¬r < w
⊢ w + 1 > 0
-- Mathlib/Order/SemiconjSup.lean
theorem orderIso_comp [Preorder α] [Preorder β] [Preorder γ] {f : α → β} {g : β → α}
    (h : IsOrderRightAdjoint f g) (e : β ≃o γ) : IsOrderRightAdjoint (e ∘ f) (g ∘ e.symm) :=
  fun y => by simpa [e.le_symm_apply] using h (e.symm y)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : β ≃o γ
y : γ
⊢ IsLUB {x | (⇑e ∘ f) x ≤ y} ((g ∘ ⇑e.symm) y)

Tactic:
simpa [e.le_symm_apply] using h (e.symm y)

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem unary_relation_sInf_iff {α : Type*} (s : Set (α → Prop)) {a : α} :
    sInf s a ↔ ∀ r : α → Prop, r ∈ s → r a

Proof state:
α : Type u_8
s : Set (α → Prop)
a : α
⊢ sInf s a ↔ ∀ r ∈ s, r a

Tactic:
rw [sInf_apply]

Result:
α : Type u_8
s : Set (α → Prop)
a : α
⊢ ⨅ f, ↑f a ↔ ∀ r ∈ s, r a

Proof state:
α : Type u_8
s : Set (α → Prop)
a : α
⊢ ⨅ f, ↑f a ↔ ∀ r ∈ s, r a

Tactic:
simp [← eq_iff_iff]

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/Basic.lean
theorem one_lt_rOut_div_rIn {c : E} (f : ContDiffBump c) : 1 < f.rOut / f.rIn

Proof state:
E : Type u_1
c : E
f : ContDiffBump c
⊢ f.rIn < f.rOut

Tactic:
exact f.rIn_lt_rOut

Result:
no goals

Proof state:
E : Type u_1
c : E
f : ContDiffBump c
⊢ 1 < f.rOut / f.rIn

Tactic:
rw [one_lt_div f.rIn_pos]

Result:
E : Type u_1
c : E
f : ContDiffBump c
⊢ f.rIn < f.rOut